Added "make check"

This commit is contained in:
Clifford Wolf 2015-10-14 23:26:04 +02:00
parent 6783abd994
commit 07f28068f6
3 changed files with 33 additions and 2 deletions

2
.gitignore vendored
View File

@ -20,6 +20,8 @@
/testbench_synth.exe /testbench_synth.exe
/testbench.gtkw /testbench.gtkw
/testbench.vcd /testbench.vcd
/check.smt2
/check.vcd
/synth.log /synth.log
/synth.v /synth.v
.*.swp .*.swp

View File

@ -14,6 +14,15 @@ testbench.vcd: testbench.exe firmware/firmware.hex
view: testbench.vcd view: testbench.vcd
gtkwave $< testbench.gtkw 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 test_sp: testbench_sp.exe firmware/firmware.hex
vvp -N testbench_sp.exe 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 gawk '/^-+$$/ { y=tolower(x); gsub("[^a-z0-9]+", "-", y); gsub("-$$", "", y); printf("- [%s](#%s)\n", x, y); } { x=$$0; }' README.md
clean: 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 \ 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 .PHONY: test view test_sp test_axi test_synth toc clean

View File

@ -1092,6 +1092,26 @@ module picorv32 #(
reg_next_pc[1:0] <= 0; reg_next_pc[1:0] <= 0;
current_pc = 'bx; current_pc = 'bx;
end 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 endmodule