From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 12 Aug 2015 10:56:20 +0000 (+0200)
Subject: Added SMV back-end 'test_cells.sh' script
X-Git-Tag: yosys-0.6~198^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f81bf9bdea7f99602bc2c7f0d43f1058a716508e;p=yosys.git

Added SMV back-end 'test_cells.sh' script
---

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.'
+