aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/test_cells.sh
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-12-25 17:52:31 +0100
committerClifford Wolf <clifford@clifford.at>2014-12-25 17:52:31 +0100
commit68233baa1f3d6e3dcfec20583b0f37202035a589 (patch)
treee2f093c943e6a30588e69e52bb1206043af9a9ff /backends/smt2/test_cells.sh
parent7dece74fae69e80349f9848ea2b9a09252de2c23 (diff)
downloadyosys-68233baa1f3d6e3dcfec20583b0f37202035a589.tar.gz
yosys-68233baa1f3d6e3dcfec20583b0f37202035a589.tar.bz2
yosys-68233baa1f3d6e3dcfec20583b0f37202035a589.zip
Various fixes and improvements in write_smt2
Diffstat (limited to 'backends/smt2/test_cells.sh')
-rw-r--r--backends/smt2/test_cells.sh45
1 files changed, 45 insertions, 0 deletions
diff --git a/backends/smt2/test_cells.sh b/backends/smt2/test_cells.sh
new file mode 100644
index 000000000..28d5c57f5
--- /dev/null
+++ b/backends/smt2/test_cells.sh
@@ -0,0 +1,45 @@
+#!/bin/bash
+
+set -ex
+
+rm -rf test_cells
+mkdir test_cells
+cd test_cells
+
+../../../yosys -p 'test_cell -n 2 -w test all /$alu /$macc /$fa /$lcu /$lut /$shift /$shiftx /$div /$mod'
+
+cat > miter.tpl <<- EOT
+; #model# (set-option :produce-models true)
+(set-logic QF_UFBV)
+%%
+(declare-fun s () miter_s)
+(assert (|miter_n trigger| s))
+(check-sat)
+; #model# (get-value ((|miter_n in_A| s) (|miter_n in_B| s) (|miter_n gold_Y| s) (|miter_n gate_Y| s) (|miter_n trigger| s)))
+EOT
+
+for x in test_*.il; do
+ x=${x%.il}
+ cat > $x.ys <<- EOT
+ read_ilang $x.il
+ copy gold gate
+
+ cd gate
+ techmap; opt; abc;;
+ cd ..
+
+ miter -equiv -flatten -make_outputs gold gate miter
+ hierarchy -check -top miter
+
+ dump
+ write_smt2 -bv -tpl miter.tpl $x.smt2
+ EOT
+ ../../../yosys $x.ys
+ cvc4 $x.smt2 > $x.result
+ if ! grep unsat $x.result; then
+ echo "Proof failed! Extracting model..."
+ sed -i 's/^; #model# //' $x.smt2
+ cvc4 $x.smt2
+ exit 1
+ fi
+done