blob: aea5bfffba1594c4e0ca6da73f4f5bb4736ac4e7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
#!/usr/bin/env bash
if [ $# -lt 1 ]; then
echo "Usage: $0 nextpnr_mode solve_mode"
exit -1
fi
case $1 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 -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
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"
if [ $2 = "sat" ]; then
do_sat $1
elif [ $2 = "smt" ]; then
do_smt $1
fi
|
