From 28fe45ffe929c2f6788314e5ff27923c8dc770b6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 29 Aug 2016 17:23:00 +0200 Subject: Added more asserts to picorv32, more smtbmc examples --- Makefile | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'Makefile') 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 -- cgit