aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile12
1 files changed, 8 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index c585588..eb3aa8a 100644
--- a/Makefile
+++ b/Makefile
@@ -19,9 +19,13 @@ testbench.vcd: testbench.vvp firmware/firmware.hex
view: testbench.vcd
gtkwave $< testbench.gtkw
-check: check.smt2
- yosys-smtbmc -t 30 --dump-vcd check.vcd check.smt2
- yosys-smtbmc -t 30 --dump-vcd check.vcd -i check.smt2
+check-z3: check.smt2
+ yosys-smtbmc -s z3 -t 30 --dump-vcd check.vcd check.smt2
+ yosys-smtbmc -s z3 -t 30 --dump-vcd check.vcd -i check.smt2
+
+check-yices: check.smt2
+ yosys-smtbmc -s yices -t 30 --dump-vcd check.vcd check.smt2
+ yosys-smtbmc -s yices -t 30 --dump-vcd check.vcd -i check.smt2
check.smt2: picorv32.v
yosys -v2 -p 'read_verilog -formal picorv32.v' \
@@ -133,5 +137,5 @@ clean:
firmware/firmware.elf firmware/firmware.bin firmware/firmware.hex firmware/firmware.map \
testbench.vvp testbench_sp.vvp testbench_synth.vvp testbench.vcd testbench.trace
-.PHONY: test view test_sp test_axi test_synth download-tools toc clean
+.PHONY: test view test_sp test_axi test_synth check-z3 check-yices download-tools build-tools toc clean