diff options
Diffstat (limited to 'backends/smt2/test_cells.sh')
| -rw-r--r-- | backends/smt2/test_cells.sh | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/backends/smt2/test_cells.sh b/backends/smt2/test_cells.sh index 28d5c57f..34adb7af 100644 --- a/backends/smt2/test_cells.sh +++ b/backends/smt2/test_cells.sh @@ -6,7 +6,7 @@ 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' +../../../yosys -p 'test_cell -muxdiv -w test all /$alu /$macc /$fa /$lcu /$lut /$shift /$shiftx' cat > miter.tpl <<- EOT ; #model# (set-option :produce-models true) @@ -18,7 +18,7 @@ cat > miter.tpl <<- EOT ; #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 +for x in $(set +x; ls test_*.il | sort -R); do x=${x%.il} cat > $x.ys <<- EOT read_ilang $x.il @@ -34,8 +34,11 @@ for x in test_*.il; do dump write_smt2 -bv -tpl miter.tpl $x.smt2 EOT - ../../../yosys $x.ys - cvc4 $x.smt2 > $x.result + ../../../yosys -q $x.ys + if ! cvc4 $x.smt2 > $x.result; then + cat $x.result + exit 1 + fi if ! grep unsat $x.result; then echo "Proof failed! Extracting model..." sed -i 's/^; #model# //' $x.smt2 @@ -43,3 +46,10 @@ for x in test_*.il; do exit 1 fi done + +set +x +echo "" +echo " All tests passed." +echo "" +exit 0 + |