From 07f28068f6f095b88c826a9f8e991f7651400d9e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 14 Oct 2015 23:26:04 +0200 Subject: [PATCH] Added "make check" --- .gitignore | 2 ++ Makefile | 13 +++++++++++-- picorv32.v | 20 ++++++++++++++++++++ 3 files changed, 33 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index bca5e64..66f233f 100644 --- a/.gitignore +++ b/.gitignore @@ -20,6 +20,8 @@ /testbench_synth.exe /testbench.gtkw /testbench.vcd +/check.smt2 +/check.vcd /synth.log /synth.v .*.swp 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 diff --git a/picorv32.v b/picorv32.v index ebe65bb..7f38a2e 100644 --- a/picorv32.v +++ b/picorv32.v @@ -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