diff options
| author | Clifford Wolf <clifford@clifford.at> | 2015-10-15 15:45:19 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2015-10-15 15:45:19 +0200 |
| commit | 8eaeebf486084216d1349fa89c18195e79ab14e0 (patch) | |
| tree | fe063abe8432a3da3477c6bc7fda5f67d69b3531 | |
| parent | 07f28068f6f095b88c826a9f8e991f7651400d9e (diff) | |
| download | picorv32-8eaeebf486084216d1349fa89c18195e79ab14e0.tar.gz picorv32-8eaeebf486084216d1349fa89c18195e79ab14e0.zip | |
Progress in "make check"
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | picorv32.v | 40 |
2 files changed, 31 insertions, 13 deletions
@@ -15,8 +15,8 @@ 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 + yosys-smtbmc -t 30 -c check.vcd check.smt2 + yosys-smtbmc -t 30 -c check.vcd -i check.smt2 check.smt2: picorv32.v yosys -v2 -p 'read_verilog -formal picorv32.v' \ @@ -27,6 +27,11 @@ `define debug(debug_command) `endif +`ifdef FORMAL + `define FORMAL_KEEP (* keep *) +`else + `define FORMAL_KEEP +`endif /*************************************************************** * picorv32 @@ -304,9 +309,9 @@ module picorv32 #( assign is_rdcycle_rdcycleh_rdinstr_rdinstrh = |{instr_rdcycle, instr_rdcycleh, instr_rdinstr, instr_rdinstrh}; reg [63:0] new_ascii_instr; - reg [63:0] ascii_instr; + `FORMAL_KEEP reg [63:0] ascii_instr; - always @* begin + always @(posedge clk) begin new_ascii_instr = ""; if (instr_lui) new_ascii_instr = "lui"; if (instr_auipc) new_ascii_instr = "auipc"; @@ -363,7 +368,7 @@ module picorv32 #( if (instr_timer) new_ascii_instr = "timer"; if (decoder_trigger_q) - ascii_instr = new_ascii_instr; + ascii_instr <= new_ascii_instr; end always @(posedge clk) begin @@ -402,9 +407,7 @@ module picorv32 #( end if (decoder_trigger && !decoder_pseudo_trigger) begin - if (WITH_PCPI) begin - pcpi_insn <= mem_rdata_q; - end + pcpi_insn <= WITH_PCPI ? mem_rdata_q : 'bx; instr_beq <= is_beq_bne_blt_bge_bltu_bgeu && mem_rdata_q[14:12] == 3'b000; instr_bne <= is_beq_bne_blt_bge_bltu_bgeu && mem_rdata_q[14:12] == 3'b001; @@ -511,7 +514,7 @@ module picorv32 #( reg [7:0] cpu_state; reg [1:0] irq_state; - reg [127:0] ascii_state; + `FORMAL_KEEP reg [127:0] ascii_state; always @* begin ascii_state = ""; @@ -1097,18 +1100,33 @@ module picorv32 #( // Formal Verification `ifdef FORMAL reg [3:0] cycle = 0; + always @(posedge clk) + if (~&cycle) cycle <= cycle + 1; - always @(posedge clk) begin - if (~&cycle) - cycle <= cycle + 1; - end + reg [4:0] last_mem_ready; + always @(posedge clk) + last_mem_ready <= {last_mem_ready, mem_ready}; + assume property (|last_mem_ready); + reg ok; always @* begin assume (resetn == |cycle); if (cycle) begin // instruction fetches are read-only if (mem_valid && mem_instr) assert (mem_wstrb == 0); + + // cpu_state must be valid + ok = 0; + if (cpu_state == cpu_state_trap) ok = 1; + if (cpu_state == cpu_state_fetch) ok = 1; + if (cpu_state == cpu_state_ld_rs1) ok = 1; + if (cpu_state == cpu_state_ld_rs2) ok = ENABLE_REGS_DUALPORT; + if (cpu_state == cpu_state_exec) ok = 1; + if (cpu_state == cpu_state_shift) ok = 1; + if (cpu_state == cpu_state_stmem) ok = 1; + if (cpu_state == cpu_state_ldmem) ok = 1; + assert (ok); end end `endif |