diff options
Diffstat (limited to 'machxo2/examples')
-rw-r--r-- | machxo2/examples/.gitignore | 5 | ||||
-rw-r--r-- | machxo2/examples/README.md | 37 | ||||
-rw-r--r-- | machxo2/examples/blinky.v | 6 | ||||
-rw-r--r-- | machxo2/examples/mitertest.sh | 43 | ||||
-rw-r--r-- | machxo2/examples/simple.sh | 35 | ||||
-rw-r--r-- | machxo2/examples/simtest.sh | 37 |
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 |