Merge pull request #578 from YosysHQ/machxo2-rebase

machxo2, rebased and updated

1 files changed, 85 insertions, 0 deletions

diff --git a/machxo2/examples/mitertest.sh b/machxo2/examples/mitertest.sh
new file mode 100644
index 00000000..cfae28b7
--- /dev/null
+++ b/machxo2/examples/mitertest.sh
@@ -0,0 +1,85 @@
+#!/usr/bin/env bash
+
+if [ $# -lt 3 ]; then
+    echo "Usage: $0 prefix nextpnr_mode solve_mode"
+    exit -1
+fi
+
+if grep -q "OSCH" $1.v; then
+    echo "$1.v uses blackbox primitive OSCH and cannot be simulated."
+    exit -2
+fi
+
+case $2 in
+    "pack")
+        NEXTPNR_MODE="--pack-only"
+        ;;
+    "place")
+        NEXTPNR_MODE="--no-route"
+        ;;
+    "pnr")
+        NEXTPNR_MODE=""
+        ;;
+    *)
+        echo "nextpnr_mode string must be \"pack\", \"place\", or \"pnr\""
+        exit -3
+        ;;
+esac
+
+case $3 in
+    "sat")
+        SAT=1
+        ;;
+    "smt")
+        SMT=1
+        ;;
+    *)
+        echo "solve_mode string must be \"sat\", or \"smt\""
+        exit -4
+        ;;
+esac
+
+do_sat() {
+    ${YOSYS:-yosys} -l ${2}${1}_miter_sat.log -p "read_verilog ${1}.v
+                        rename top gold
+                        read_verilog ${2}${1}.v
+                        rename top gate
+                        read_verilog +/machxo2/cells_sim.v
+
+                        miter -equiv -make_assert -flatten gold gate ${2}${1}_miter
+                        hierarchy -top ${2}${1}_miter
+                        sat -verify -prove-asserts -tempinduct ${2}${1}_miter"
+}
+
+do_smt() {
+    ${YOSYS:-yosys} -l ${2}${1}_miter_smt.log -p "read_verilog ${1}.v
+                        rename top gold
+                        read_verilog ${2}${1}.v
+                        rename top gate
+                        read_verilog +/machxo2/cells_sim.v
+
+                        miter -equiv -make_assert gold gate ${2}${1}_miter
+                        hierarchy -top ${2}${1}_miter; proc;
+                        opt_clean
+                        write_verilog ${2}${1}_miter.v
+                        write_smt2 ${2}${1}_miter.smt2"
+
+    yosys-smtbmc -s z3 --dump-vcd ${2}${1}_miter_bmc.vcd ${2}${1}_miter.smt2
+    yosys-smtbmc -s z3 -i --dump-vcd ${2}${1}_miter_tmp.vcd ${2}${1}_miter.smt2
+}
+
+set -ex
+
+${YOSYS:-yosys} -p "read_verilog ${1}.v
+                    synth_machxo2 -noiopad -json ${1}.json"
+${NEXTPNR:-../../nextpnr-machxo2} $NEXTPNR_MODE --1200 --package QFN32 --no-iobs --json ${1}.json --write ${2}${1}.json
+${YOSYS:-yosys} -p "read_verilog -lib +/machxo2/cells_sim.v
+                    read_json ${2}${1}.json
+                    clean -purge
+                    write_verilog -noattr -norename ${2}${1}.v"
+
+if [ $3 = "sat" ]; then
+    do_sat $1 $2
+elif [ $3 = "smt" ]; then
+    do_smt $1 $2
+fi