mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 11:42:30 +00:00
33 lines
490 B
Bash
33 lines
490 B
Bash
#!/usr/bin/env bash
|
|
|
|
cat > $1.tpl <<EOT
|
|
%module main
|
|
INVARSPEC ! bool(_trigger)
|
|
EOT
|
|
|
|
cat > $1.ys <<EOT
|
|
echo on
|
|
|
|
read_rtlil $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
|
|
|