caiyu/nextpnr
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
William D. Jones 2020-11-28 21:08:09 -05:00 committed by gatecat
parent 5838662b2f
commit 4f042eac53
6 changed files with 145 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
machxo2/examples/.gitignore vendored
View File

@ -1,4 +1,7 @@
pnrblinky.v
/blinky_simtest
*.vcd
*.png
pack*.v
place*.v
pnr*.v
abc.history

37
machxo2/examples/README.md
View File

@ -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

6
machxo2/examples/blinky.v
View File

@ -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)

43
machxo2/examples/mitertest.sh Normal file
View File

@ -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"

35
machxo2/examples/simple.sh
View File

@ -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"

37
machxo2/examples/simtest.sh
View File

@ -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