diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-08-26 23:56:04 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-08-26 23:56:04 +0200 |
| commit | 72158ba4a589cf838b9c474798e4dce9315fa47c (patch) | |
| tree | 69d6200388cb2342bea7e135a368db02360de7a2 /picorv32.v | |
| parent | d1d3c3c5e199e6b73aca26e35abb1d1abdfd2de8 (diff) | |
| download | picorv32-72158ba4a589cf838b9c474798e4dce9315fa47c.tar.gz picorv32-72158ba4a589cf838b9c474798e4dce9315fa47c.zip | |
Some minor cleanups
Diffstat (limited to 'picorv32.v')
| -rw-r--r-- | picorv32.v | 22 |
1 files changed, 10 insertions, 12 deletions
@@ -1168,8 +1168,10 @@ module picorv32 #( decoder_pseudo_trigger_q <= decoder_pseudo_trigger; do_waitirq <= 0; - if (ENABLE_TRACE) - trace_valid <= 0; + trace_valid <= 0; + + if (!ENABLE_TRACE) + trace_data <= 'bx; if (!resetn) begin reg_pc <= PROGADDR_RESET; @@ -1663,19 +1665,15 @@ module picorv32 #( // Formal Verification `ifdef FORMAL - reg [3:0] cycle = 0; - always @(posedge clk) - if (~&cycle) cycle <= cycle + 1; - - reg [4:0] last_mem_ready; + reg [3:0] last_mem_nowait; always @(posedge clk) - last_mem_ready <= {last_mem_ready, mem_ready}; - restrict property (|last_mem_ready); + last_mem_nowait <= {last_mem_nowait, mem_ready || !mem_valid}; + restrict property (|last_mem_nowait || mem_ready || !mem_valid); reg ok; always @* begin - restrict (resetn == |cycle); - if (cycle) begin + restrict (resetn == !$initstate); + if (!$initstate) begin // instruction fetches are read-only if (mem_valid && mem_instr) assert (mem_wstrb == 0); @@ -1685,7 +1683,7 @@ module picorv32 #( 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_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; |