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 | |
parent | 6783abd994ffb91f7e1b39d1d656419a2881211f (diff) | |
download | picorv32-07f28068f6f095b88c826a9f8e991f7651400d9e.tar.gz picorv32-07f28068f6f095b88c826a9f8e991f7651400d9e.zip |
Added "make check"
-rw-r--r-- | .gitignore | 2 | ||||
-rw-r--r-- | Makefile | 13 | ||||
-rw-r--r-- | picorv32.v | 20 |
3 files changed, 33 insertions, 2 deletions
@@ -20,6 +20,8 @@ /testbench_synth.exe /testbench.gtkw /testbench.vcd +/check.smt2 +/check.vcd /synth.log /synth.v .*.swp @@ -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 @@ -1092,6 +1092,26 @@ module picorv32 #( reg_next_pc[1:0] <= 0; current_pc = 'bx; end + + + // Formal Verification +`ifdef FORMAL + reg [3:0] cycle = 0; + + always @(posedge clk) begin + if (~&cycle) + cycle <= cycle + 1; + end + + always @* begin + assume (resetn == |cycle); + if (cycle) begin + // instruction fetches are read-only + if (mem_valid && mem_instr) + assert (mem_wstrb == 0); + end + end +`endif endmodule |