2023-08-11 20:59:39 -05:00
|
|
|
#!/usr/bin/env bash
|
2015-06-18 09:29:11 -05:00
|
|
|
|
|
|
|
|
cat > $1.tpl <<EOT
|
|
|
|
|
%module main
|
|
|
|
|
INVARSPEC ! bool(_trigger)
|
|
|
|
|
EOT
|
|
|
|
|
|
|
|
|
|
cat > $1.ys <<EOT
|
|
|
|
|
echo on
|
|
|
|
|
|
|
|
|
|
read_ilang $1.il
|
|
|
|
|
hierarchy; proc; opt
|
|
|
|
|
rename -top uut
|
|
|
|
|
design -save gold
|
|
|
|
|
|
|
|
|
|
synth
|
|
|
|
|
design -stash gate
|
|
|
|
|
|
|
|
|
|
design -copy-from gold -as gold uut
|
|
|
|
|
design -copy-from gate -as gate uut
|
|
|
|
|
miter -equiv -flatten gold gate main
|
|
|
|
|
hierarchy -top main
|
|
|
|
|
|
|
|
|
|
dump
|
|
|
|
|
write_smv -tpl $1.tpl $1.smv
|
|
|
|
|
EOT
|
|
|
|
|
|
|
|
|
|
set -ex
|
|
|
|
|
|
|
|
|
|
../../yosys -l $1.log -q $1.ys
|
|
|
|
|
NuSMV -bmc $1.smv >> $1.log
|
|
|
|
|
grep "^-- invariant .* is true" $1.log
|
|
|
|
|
|
