summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2015-06-18 16:29:11 +0200
committerClifford Wolf <clifford@clifford.at>2015-06-18 16:29:11 +0200
commit8a86162ae9a4e2939af162edfc6fa281931f786e (patch)
tree185a9b2bc65b00280951fce4c7eccaf7ae0f6d77 /tests
parent8e84418225b9e9a22f4a7c4493aa551e596f5e9d (diff)
Progress in SMV back-end
Diffstat (limited to 'tests')
-rw-r--r--tests/smv/.gitignore1
-rw-r--r--tests/smv/run-single.sh33
-rwxr-xr-xtests/smv/run-test.sh19
3 files changed, 53 insertions, 0 deletions
diff --git a/tests/smv/.gitignore b/tests/smv/.gitignore
new file mode 100644
index 00000000..9c595a6f
--- /dev/null
+++ b/tests/smv/.gitignore
@@ -0,0 +1 @@
+temp
diff --git a/tests/smv/run-single.sh b/tests/smv/run-single.sh
new file mode 100644
index 00000000..a261f4ea
--- /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
+
diff --git a/tests/smv/run-test.sh b/tests/smv/run-test.sh
new file mode 100755
index 00000000..c61f67d3
--- /dev/null
+++ b/tests/smv/run-test.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+set -ex
+
+rm -rf temp
+mkdir -p temp
+
+../../yosys -p 'test_cell -muxdiv -w temp/test all'
+rm -f temp/test_{alu,fa,lcu,lut,macc}_*
+
+cat > temp/makefile << "EOT"
+all: $(addsuffix .ok,$(basename $(wildcard temp/test_*.il)))
+%.ok: %.il
+ bash run-single.sh $(basename $<)
+ touch $@
+EOT
+
+${MAKE:-make} -f temp/makefile
+