1 files changed, 33 insertions, 0 deletions
diff --git a/tests/smv/run-single.sh b/tests/smv/run-single.sh
new file mode 100644
index 000000000..a261f4ea6
--- /dev/null
+++ b/tests/smv/run-single.sh
@@ -0,0 +1,33 @@
+#!/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
+