34 lines
482 B
Bash
34 lines
482 B
Bash
|
#!/bin/bash
|
||
|
|
|
||
|
|
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
|
||
|
|
|