diff options
author | William D. Jones <thor0505@comcast.net> | 2020-11-28 21:43:03 -0500 |
---|---|---|
committer | gatecat <gatecat@ds0.me> | 2021-02-12 10:36:59 +0000 |
commit | 6ce2edc2f109f81adfb143d2732dabe6fc4e36de (patch) | |
tree | 6b61f9799ebf872e4540391e37f6a727f5e3945b /machxo2/examples/mitertest.sh | |
parent | 4f042eac5338c789ad90ac10dc2a9d8e92ce1acd (diff) | |
download | nextpnr-6ce2edc2f109f81adfb143d2732dabe6fc4e36de.tar.gz nextpnr-6ce2edc2f109f81adfb143d2732dabe6fc4e36de.tar.bz2 nextpnr-6ce2edc2f109f81adfb143d2732dabe6fc4e36de.zip |
machxo2: Add SMT mode to mitertest.sh
Diffstat (limited to 'machxo2/examples/mitertest.sh')
-rw-r--r-- | machxo2/examples/mitertest.sh | 61 |
1 files changed, 50 insertions, 11 deletions
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 |