machxo2: Rework examples to test pack, place, and route phases.

6 files changed, 145 insertions, 18 deletions

diff --git a/machxo2/examples/.gitignore b/machxo2/examples/.gitignore
index f1ee6a8a..a4c8185f 100644
--- a/machxo2/examples/.gitignore
+++ b/machxo2/examples/.gitignore
@@ -1,4 +1,7 @@
-pnrblinky.v
 /blinky_simtest
 *.vcd
+*.png
+pack*.v
+place*.v
+pnr*.v
 abc.history
diff --git a/machxo2/examples/README.md b/machxo2/examples/README.md
index 87f50f6d..aac80fb4 100644
--- a/machxo2/examples/README.md
+++ b/machxo2/examples/README.md
@@ -2,18 +2,37 @@
 
 This contains a simple example of running `nextpnr-machxo2`:
 
-* `simple.sh` generates JSON output (`pnrblinky.json`) of a classic blinky
-  example from `blinky.v`.
+* `simple.sh` generates JSON output (`{pack,place,pnr}blinky.json`) of a
+  classic blinky example from `blinky.v`.
 * `simtest.sh` will use `yosys` to generate a Verilog file from
-  `pnrblinky.json`, called `pnrblinky.v`. It will then and compare
-  `pnrblinky.v`'s simulation behavior to the original verilog file (`blinky.v`)
-  using the [`iverilog`](http://iverilog.icarus.com) compiler and `vvp`
-  runtime. This is known as post-place-and-route simulation.
+  `{pack,place,pnr}blinky.json`, called `{pack,place,pnr}blinky.v`. It will
+  then and compare `{pack,place,pnr}blinky.v`'s simulation behavior to the
+  original verilog file (`blinky.v`) using the [`iverilog`](http://iverilog.icarus.com)
+  compiler and `vvp` runtime. This is known as post-place-and-route simulation.
+* `mitertest.sh` is similar to `simtest.sh`, but more comprehensive. This
+  script creates a [miter circuit](https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/Equivalence_Checking_11_30_08.pdf)
+  to compare the output port values of `{pack,place,pnr}blinky.v` against the
+  original `blinky.v` _when both modules are fed the same values on their input
+  ports._
 
-As `nextpnr-machxo2` is developed the contents `simple.sh` and `simtest.sh`
-are subject to change.
+  All possible inputs and resulting outputs can be tested in reasonable time by
+  using yosys' built-in SAT solver.
 
-## Environment Variables For `simple.sh` And `simtest.sh`
+As `nextpnr-machxo2` is developed the contents `simple.sh`, `simtest.sh`, and
+`mitertest.sh` are subject to change.
+
+## How To Run
+
+Each `sh` script runs yosys and nextpnr to validate a blinky design in various
+ways. The `mode` argument to each script- `pack`, `place`, or `pnr`- stop
+`nextpnr-machxo2` after the specified phase and writes out a JSON file of the
+results in `{pack,place,pnr}blinky.json`; `pnr` runs all of the Pack, Place,
+and Route phases.
+
+To keep file count lower, all yosys scripts are written inline inside the
+`sh` scripts using the `-p` option.
+
+## Environment Variables For Scripts
 
 * `YOSYS`- Set to the location of the `yosys` binary to test. Defaults to the
   `yosys` on the path. You may want to set this to a `yosys` binary in your
diff --git a/machxo2/examples/blinky.v b/machxo2/examples/blinky.v
index 2137ad58..57bad543 100644
--- a/machxo2/examples/blinky.v
+++ b/machxo2/examples/blinky.v
@@ -1,6 +1,10 @@
 module top(input clk, rst, output [7:0] leds);
 
-// TODO: Test miter circuit without reset value.
+// TODO: Test miter circuit without reset value. SAT and SMT diverge without
+// reset value (SAT succeeds, SMT fails). I haven't figured out the correct
+// init set of options to make SAT fail.
+// "sat -verify -prove-asserts -set-init-def -seq 1 miter" causes assertion
+// failure in yosys.
 reg [7:0] ctr = 8'h00;
 always @(posedge clk)
 	if (rst)
diff --git a/machxo2/examples/mitertest.sh b/machxo2/examples/mitertest.sh
new file mode 100644
index 00000000..e5cc5173
--- /dev/null
+++ b/machxo2/examples/mitertest.sh
@@ -0,0 +1,43 @@
+#!/usr/bin/env bash
+
+if [ $# -lt 1 ]; then
+    echo "Usage: $0 mode"
+    exit -1
+fi
+
+case $1 in
+    "pack")
+        NEXTPNR_MODE="--pack-only"
+        ;;
+    "place")
+        NEXTPNR_MODE="--no-route"
+        ;;
+    "pnr")
+        NEXTPNR_MODE=""
+        ;;
+    *)
+        echo "Mode string must be \"pack\", \"place\", or \"pnr\""
+        exit -2
+        ;;
+esac
+
+set -ex
+
+${YOSYS:-yosys} -p "read_verilog blinky.v
+                    synth_machxo2 -noiopad -json blinky.json
+                    show -format png -prefix blinky"
+${NEXTPNR:-../../nextpnr-machxo2} $NEXTPNR_MODE --1200 --no-iobs --json blinky.json --write ${1}blinky.json
+${YOSYS:-yosys} -p "read_verilog -lib +/machxo2/cells_sim.v
+                    read_json ${1}blinky.json
+                    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"
diff --git a/machxo2/examples/simple.sh b/machxo2/examples/simple.sh
index 9eb06886..91fa4b91 100644
--- a/machxo2/examples/simple.sh
+++ b/machxo2/examples/simple.sh
@@ -1,5 +1,34 @@
 #!/usr/bin/env bash
+
+if [ $# -lt 1 ]; then
+    echo "Usage: $0 mode"
+    exit -1
+fi
+
+case $1 in
+    "pack")
+        NEXTPNR_MODE="--pack-only"
+        ;;
+    "place")
+        NEXTPNR_MODE="--no-route"
+        ;;
+    "pnr")
+        NEXTPNR_MODE=""
+        ;;
+    *)
+        echo "Mode string must be \"pack\", \"place\", or \"pnr\""
+        exit -2
+        ;;
+esac
+
 set -ex
-${YOSYS:yosys} -p "synth_machxo2 -json blinky.json" blinky.v
-${NEXTPNR:-../../nextpnr-machxo2} --json blinky.json --write pnrblinky.json
-${YOSYS:yosys} -p "read_verilog -lib +/machxo2/cells_sim.v; read_json pnrblinky.json; dump -o blinky.il; show -format png -prefix blinky"
+
+${YOSYS:-yosys} -p "read_verilog blinky.v
+                    synth_machxo2 -json blinky.json
+                    show -format png -prefix blinky"
+${NEXTPNR:-../../nextpnr-machxo2} $NEXTPNR_MODE --1200 --no-iobs --json blinky.json --write ${1}blinky.json
+${YOSYS:-yosys} -p "read_verilog -lib +/machxo2/cells_sim.v
+                    read_json ${1}blinky.json
+                    clean -purge
+                    show -format png -prefix ${1}blinky
+                    write_verilog -noattr -norename ${1}blinky.v"
diff --git a/machxo2/examples/simtest.sh b/machxo2/examples/simtest.sh
index 4cb8d5ca..ff35bbd6 100644
--- a/machxo2/examples/simtest.sh
+++ b/machxo2/examples/simtest.sh
@@ -1,7 +1,36 @@
 #!/usr/bin/env bash
+
+if [ $# -lt 1 ]; then
+    echo "Usage: $0 mode"
+    exit -1
+fi
+
+case $1 in
+    "pack")
+        NEXTPNR_MODE="--pack-only"
+        ;;
+    "place")
+        NEXTPNR_MODE="--no-route"
+        ;;
+    "pnr")
+        NEXTPNR_MODE=""
+        ;;
+    *)
+        echo "Mode string must be \"pack\", \"place\", or \"pnr\""
+        exit -2
+        ;;
+esac
+
 set -ex
-${YOSYS:-yosys} -p "synth_machxo2 -json blinky.json" blinky.v
-${NEXTPNR:-../../nextpnr-machxo2} --no-iobs --json blinky.json --write pnrblinky.json
-${YOSYS:-yosys} -p "read_json blinky.json; write_verilog  -noattr -norename pnrblinky.v"
-iverilog -o blinky_simtest ${CELLS_SIM:-`${YOSYS:yosys}-config --datdir/machxo2/cells_sim.v`} blinky_tb.v pnrblinky.v
+
+${YOSYS:-yosys} -p "read_verilog blinky.v
+                    synth_machxo2 -json blinky.json
+                    show -format png -prefix blinky"
+${NEXTPNR:-../../nextpnr-machxo2} $NEXTPNR_MODE --1200 --no-iobs --json blinky.json --write ${1}blinky.json
+${YOSYS:-yosys} -p "read_verilog -lib +/machxo2/cells_sim.v
+                    read_json ${1}blinky.json
+                    clean -purge
+                    show -format png -prefix ${1}blinky
+                    write_verilog -noattr -norename ${1}blinky.v"
+iverilog -o blinky_simtest ${CELLS_SIM:-`${YOSYS:yosys}-config --datdir/machxo2/cells_sim.v`} blinky_tb.v ${1}blinky.v
 vvp -N ./blinky_simtest