From f81bf9bdea7f99602bc2c7f0d43f1058a716508e Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 12 Aug 2015 12:56:20 +0200
Subject: [PATCH] Added SMV back-end 'test_cells.sh' script

---
 backends/smv/test_cells.sh | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 backends/smv/test_cells.sh

diff --git a/backends/smv/test_cells.sh b/backends/smv/test_cells.sh
new file mode 100644
index 000000000..63de465c0
--- /dev/null
+++ b/backends/smv/test_cells.sh
@@ -0,0 +1,33 @@
+#!/bin/bash
+
+set -ex
+
+rm -rf test_cells.tmp
+mkdir -p test_cells.tmp
+cd test_cells.tmp
+
+# don't test $mul to reduce runtime
+# don't test $div and $mod to reduce runtime and avoid "div by zero" message
+../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$macc /$mul /$div /$mod'
+
+cat > template.txt << "EOT"
+%module main
+  INVARSPEC ! bool(_trigger);
+EOT
+
+for fn in test_*.il; do
+	../../../yosys -p "
+		read_ilang $fn
+		rename gold gate
+		synth
+
+		read_ilang $fn
+		miter -equiv -flatten gold gate main
+		hierarchy -top main
+		write_smv -tpl template.txt ${fn#.il}.smv
+	"
+	nuXmv -dynamic ${fn#.il}.smv > ${fn#.il}.out
+done
+
+grep '^-- invariant .* is false' *.out || echo 'All OK.'
+
-- 
2.30.2