Fix bug where an IRQ can fire during load/store dphase, followed by dphase bus exception.

Result was that the exception would sample the IRQ vector PC rather than the load/store instruction PC.
Fix by fencing off on in-flight dphases before asserting the IRQ. This adds a cycle of jitter
to IRQs, but is required for correct operation without adding a full exception-gathering pipeline.

doc/sections/csr.adoc

@@ -5,7 +5,7 @@ The RISC-V privileged specification affords flexibility as to which CSRs are imp
 All CSRs are 32-bit; MXLEN is fixed at 32 bits on Hazard3. All CSR addresses not listed in this section are unimplemented. Accessing an unimplemented CSR will cause an illegal instruction exception (`mcause` = 2). This includes all U-mode and S-mode CSRs.
 
 
-IMPORTANT: The https://github.com/riscv/riscv-isa-manual/releases/download/Ratified-IMFDQC-and-Priv-v1.11/riscv-privileged-20190608.pdf[RISC-V Privileged Specification] should be your primary reference for writing software to run on Hazard3. This section specifies those details which are left implementation-defined by the RISC-V Privileged Specification, for sake of completeness, but portable RISC-V software should not rely on these details.
+IMPORTANT: The https://github.com/riscv/riscv-isa-manual/releases/download/Priv-v1.12/riscv-privileged-20211203.pdf[RISC-V Privileged Specification] should be your primary reference for writing software to run on Hazard3. This section specifies those details which are left implementation-defined by the RISC-V Privileged Specification, for sake of completeness, but portable RISC-V software should not rely on these details.
 
 === Standard M-mode Identification CSRs
 

doc/sections/instruction_timings.adoc

@@ -32,7 +32,7 @@ All timings are given assuming perfect bus behaviour (no downstream bus stalls).
 | `lui rd, imm` | 1 |
 | `auipc rd, imm` | 1 |
 3+| Control Transfer
-| `jal rd, label` | 2footnote:unaligned_branch[A branch to a 32-bit instruction which is not 32-bit-aligned requires one additional cycle, because two naturally aligned bus cycles are required to fetch the target instruction.]|
+| `jal rd, label` | 2footnote:unaligned_branch[A jump or branch to a 32-bit instruction which is not 32-bit-aligned requires one additional cycle, because two naturally aligned bus cycles are required to fetch the target instruction.]|
 | `jalr rd, rs1, imm` | 2footnote:unaligned_branch[] |
 | `beq rs1, rs2, label`| 1 or 2footnote:unaligned_branch[] | 1 if nontaken, 2 if taken.
 | `bne rs1, rs2, label`| 1 or 2footnote:unaligned_branch[] | 1 if nontaken, 2 if taken.

hdl/hazard3_csr.v

@@ -1040,14 +1040,24 @@ assign trap_addr =
 assign trap_is_irq = DEBUG_SUPPORT && (want_halt_except || want_halt_irq) ?
 	!want_halt_except : !exception_req_any;
 
+// When there is a loadstore dphase pending, we block off the IRQ trap
+// request, but still assert the trap_enter_soon flag. This blocks issue of
+// further load/stores which have not yet been locked into aphase, so the IRQ
+// can eventually go through. It's not safe to enter an IRQ when a dphase is
+// in progress, because that dphase could subsequently except, and sample the
+// IRQ vector PC instead of the load/store instruction PC.
+
 // delay_irq_entry also applies to IRQ-like debug entries.
 assign trap_enter_vld =
 	CSR_M_TRAP && (exception_req_any ||
-		!delay_irq_entry && !debug_mode && irq_active) ||
+		!delay_irq_entry && !debug_mode && irq_active && !loadstore_dphase_pending) ||
 	DEBUG_SUPPORT && (
 		(!delay_irq_entry && want_halt_irq) || want_halt_except || pending_dbg_resume);
 
-assign trap_enter_soon = trap_enter_vld || (DEBUG_SUPPORT && want_halt_irq_if_no_exception);
+assign trap_enter_soon = trap_enter_vld || (
+	|DEBUG_SUPPORT && want_halt_irq_if_no_exception ||
+	!delay_irq_entry && !debug_mode && irq_active && loadstore_dphase_pending
+);
 
 assign mcause_irq_next = !exception_req_any;
 assign mcause_code_next = exception_req_any ? {2'h0, except} : mcause_irq_num;
@@ -1105,10 +1115,18 @@ always @ (posedge clk) begin
 	//   and an exception by e.g. a left-behind store data phase would sample the
 	//   wrong PC.
 	//
-	// - Except -> IRQ: would need to re-set mstatus.mie first
+	// - Except -> IRQ: would need to re-set mstatus.mie first, shouldn't happen
+	//
+	// Sole exclusion is mret. We can return from an interrupt/exception and take
+	// a new interrupt on the next cycle.
 
-	if ($past(trap_enter_vld && trap_enter_rdy))
+	if ($past(trap_enter_vld && trap_enter_rdy && except != EXCEPT_MRET))
 		assert(!(trap_enter_vld && trap_enter_rdy));
+
+	// Just to stress that this is the the only case:
+	if (trap_enter_vld && trap_enter_rdy && $past(trap_enter_vld && trap_enter_rdy))
+		assert($past(except == EXCEPT_MRET));
+
 end
 
 `endif

test/formal/bus_compliance_2port/Makefile

@@ -1,5 +1,8 @@
 DOTF=tb.f
 TOP=tb
 YOSYS_SMT_SOLVER=boolector
+DEPTH=25
+
+all: bmc
 
 include $(SCRIPTS)/formal.mk

test/formal/common/ahbl_master_assertions.v

@@ -96,7 +96,7 @@ always @ (posedge clk) if (rst_n) begin: dst_ahbl_req_properties
 			assert(src_haddr == src_addr_dph + W_DATA / 8);
 		// No pipelining of exclusive transfers
 		if (src_excl_dph)
-			assert(!src_hexcl);
+			assert(!(src_hexcl && src_htrans[1]));
 	end
 
 	// Data phase properties: