From 449348f4591d8bcd36e81386e773e7f0f67a6233 Mon Sep 17 00:00:00 2001 From: Luke Wren Date: Tue, 7 Dec 2021 19:24:53 +0000 Subject: [PATCH] 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 | 2 +- doc/sections/instruction_timings.adoc | 2 +- hdl/hazard3_csr.v | 26 +++++++++++++++++---- test/formal/bus_compliance_2port/Makefile | 3 +++ test/formal/common/ahbl_master_assertions.v | 2 +- 5 files changed, 28 insertions(+), 7 deletions(-) diff --git a/doc/sections/csr.adoc b/doc/sections/csr.adoc index 0db2412..e639f9a 100644 --- a/doc/sections/csr.adoc +++ b/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 diff --git a/doc/sections/instruction_timings.adoc b/doc/sections/instruction_timings.adoc index 28df18e..8373308 100644 --- a/doc/sections/instruction_timings.adoc +++ b/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. diff --git a/hdl/hazard3_csr.v b/hdl/hazard3_csr.v index 5ba235d..3561568 100644 --- a/hdl/hazard3_csr.v +++ b/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 diff --git a/test/formal/bus_compliance_2port/Makefile b/test/formal/bus_compliance_2port/Makefile index 571aebe..254b0e0 100644 --- a/test/formal/bus_compliance_2port/Makefile +++ b/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 diff --git a/test/formal/common/ahbl_master_assertions.v b/test/formal/common/ahbl_master_assertions.v index 5b78909..d281c9e 100644 --- a/test/formal/common/ahbl_master_assertions.v +++ b/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: