#!/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