aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2015-10-14 23:26:04 +0200
committerClifford Wolf <clifford@clifford.at>2015-10-14 23:26:04 +0200
commit07f28068f6f095b88c826a9f8e991f7651400d9e (patch)
treeb0d97db72bf735c2772303a03cf7c3e97cf79664 /Makefile
parent6783abd994ffb91f7e1b39d1d656419a2881211f (diff)
downloadpicorv32-07f28068f6f095b88c826a9f8e991f7651400d9e.tar.gz
picorv32-07f28068f6f095b88c826a9f8e991f7651400d9e.zip
Added "make check"
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile13
1 files changed, 11 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index b5244ce..829e2d5 100644
--- a/Makefile
+++ b/Makefile
@@ -14,6 +14,15 @@ testbench.vcd: testbench.exe firmware/firmware.hex
view: testbench.vcd
gtkwave $< testbench.gtkw
+check: check.smt2
+ # yosys-smtbmc -m picorv32 check.smt2
+ yosys-smtbmc -m picorv32 -t 10 -c check.vcd -i check.smt2
+
+check.smt2: picorv32.v
+ yosys -v2 -p 'read_verilog -formal picorv32.v' \
+ -p 'prep -top picorv32 -nordff' \
+ -p 'write_smt2 -bv -mem -wires check.smt2'
+
test_sp: testbench_sp.exe firmware/firmware.hex
vvp -N testbench_sp.exe
@@ -69,9 +78,9 @@ toc:
gawk '/^-+$$/ { y=tolower(x); gsub("[^a-z0-9]+", "-", y); gsub("-$$", "", y); printf("- [%s](#%s)\n", x, y); } { x=$$0; }' README.md
clean:
- rm -vrf $(FIRMWARE_OBJS) $(TEST_OBJS) \
+ rm -vrf $(FIRMWARE_OBJS) $(TEST_OBJS) check.smt2 check.vcd synth.v synth.log \
firmware/firmware.elf firmware/firmware.bin firmware/firmware.hex firmware/firmware.map \
- synth.v testbench.exe testbench_sp.exe testbench_axi.exe testbench_synth.exe testbench.vcd
+ testbench.exe testbench_sp.exe testbench_axi.exe testbench_synth.exe testbench.vcd
.PHONY: test view test_sp test_axi test_synth toc clean