machxo2: Add SMT mode to mitertest.sh

This commit is contained in:
William D. Jones 2020-11-28 21:43:03 -05:00 committed by gatecat
parent 4f042eac53
commit 6ce2edc2f1
3 changed files with 59 additions and 11 deletions

View File

@ -1,6 +1,8 @@
/blinky_simtest
*.vcd
*.png
*.log
*.smt2
pack*.v
place*.v
pnr*.v

View File

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

View File

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