diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-10-14 23:26:04 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-10-14 23:26:04 +0200 |
commit | 07f28068f6f095b88c826a9f8e991f7651400d9e (patch) | |
tree | b0d97db72bf735c2772303a03cf7c3e97cf79664 /Makefile | |
parent | 6783abd994ffb91f7e1b39d1d656419a2881211f (diff) | |
download | picorv32-07f28068f6f095b88c826a9f8e991f7651400d9e.tar.gz picorv32-07f28068f6f095b88c826a9f8e991f7651400d9e.zip |
Added "make check"
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 13 |
1 files changed, 11 insertions, 2 deletions
@@ -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 |