machxo2: Add SMT mode to mitertest.sh

3 files changed, 60 insertions, 12 deletions

diff --git a/machxo2/examples/.gitignore b/machxo2/examples/.gitignore
index a4c8185f..87d5128b 100644
--- a/machxo2/examples/.gitignore
+++ b/machxo2/examples/.gitignore
@@ -1,6 +1,8 @@
 /blinky_simtest
 *.vcd
 *.png
+*.log
+*.smt2
 pack*.v
 place*.v
 pnr*.v
diff --git a/machxo2/examples/README.md b/machxo2/examples/README.md
index aac80fb4..e940c01c 100644
--- a/machxo2/examples/README.md
+++ b/machxo2/examples/README.md
@@ -16,7 +16,8 @@ This contains a simple example of running `nextpnr-machxo2`:
   ports._
 
   All possible inputs and resulting outputs can be tested in reasonable time by
-  using yosys' built-in SAT solver.
+  using `yosys`' built-in SAT solver or [`z3`](https://github.com/Z3Prover/z3),
+  an external SMT solver.
 
 As `nextpnr-machxo2` is developed the contents `simple.sh`, `simtest.sh`, and
 `mitertest.sh` are subject to change.
@@ -29,9 +30,15 @@ ways. The `mode` argument to each script- `pack`, `place`, or `pnr`- stop
 results in `{pack,place,pnr}blinky.json`; `pnr` runs all of the Pack, Place,
 and Route phases.
 
+`mitertest.sh` requires an additional option- `sat` or `smt`- to choose between
+verifying the miter with either yosys' built-in SAT solver, or an external
+SMT solver.
+
 To keep file count lower, all yosys scripts are written inline inside the
 `sh` scripts using the `-p` option.
 
+To clean output files, run: `rm -rf *.dot *.json *.png *.vcd *.smt2 *.log {pack,place,pnr}*.v blinky_simtest*`
+
 ## Environment Variables For Scripts
 
 * `YOSYS`- Set to the location of the `yosys` binary to test. Defaults to the
diff --git a/machxo2/examples/mitertest.sh b/machxo2/examples/mitertest.sh
index e5cc5173..aea5bfff 100644
--- a/machxo2/examples/mitertest.sh
+++ b/machxo2/examples/mitertest.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 
 if [ $# -lt 1 ]; then
-    echo "Usage: $0 mode"
+    echo "Usage: $0 nextpnr_mode solve_mode"
     exit -1
 fi
 
@@ -16,11 +16,53 @@ case $1 in
         NEXTPNR_MODE=""
         ;;
     *)
-        echo "Mode string must be \"pack\", \"place\", or \"pnr\""
+        echo "nextpnr_mode string must be \"pack\", \"place\", or \"pnr\""
         exit -2
         ;;
 esac
 
+case $2 in
+    "sat")
+        SAT=1
+        ;;
+    "smt")
+        SMT=1
+        ;;
+    *)
+        echo "solve_mode string must be \"sat\", or \"smt\""
+        exit -3
+        ;;
+esac
+
+do_sat() {
+    ${YOSYS:-yosys} -l ${1}miter_sat.log -p "read_verilog blinky.v
+                        rename top gold
+                        read_verilog ${1}blinky.v
+                        rename top gate
+                        read_verilog +/machxo2/cells_sim.v
+
+                        miter -equiv -make_assert -flatten gold gate ${1}miter
+                        hierarchy -top ${1}miter
+                        sat -verify -prove-asserts -tempinduct ${1}miter"
+}
+
+do_smt() {
+    ${YOSYS:-yosys} -l ${1}miter_smt.log -p "read_verilog blinky.v
+                        rename top gold
+                        read_verilog ${1}blinky.v
+                        rename top gate
+                        read_verilog +/machxo2/cells_sim.v
+
+                        miter -equiv -make_assert gold gate ${1}miter
+                        hierarchy -auto-top -check; proc;
+                        opt_clean
+                        write_verilog ${1}miter.v
+                        write_smt2 ${1}miter.smt2"
+
+    yosys-smtbmc -s z3 --dump-vcd ${1}miter_bmc.vcd ${1}miter.smt2
+    yosys-smtbmc -s z3 -i --dump-vcd ${1}miter_tmp.vcd ${1}miter.smt2
+}
+
 set -ex
 
 ${YOSYS:-yosys} -p "read_verilog blinky.v
@@ -32,12 +74,9 @@ ${YOSYS:-yosys} -p "read_verilog -lib +/machxo2/cells_sim.v
                     clean -purge
                     show -format png -prefix ${1}blinky
                     write_verilog -noattr -norename ${1}blinky.v"
-${YOSYS:-yosys} -p "read_verilog blinky.v
-                    rename top gold
-                    read_verilog ${1}blinky.v
-                    rename top gate
-                    read_verilog +/machxo2/cells_sim.v
-
-                    miter -equiv -make_assert -flatten gold gate miter
-                    hierarchy -top miter
-                    sat -verify -prove-asserts -tempinduct miter"
+
+if [ $2 = "sat" ]; then
+    do_sat $1
+elif [ $2 = "smt" ]; then
+    do_smt $1
+fi