Fix for issue #507

bhv/cv32e40x_wrapper.sv

@@ -33,6 +33,7 @@
   `include "cv32e40x_sleep_unit_sva.sv"
   `include "cv32e40x_rvfi_sva.sv"
   `include "cv32e40x_sequencer_sva.sv"
+  `include "cv32e40x_clic_int_controller_sva.sv"
 `endif
 
 `include "cv32e40x_wrapper.vh"
@@ -215,7 +216,12 @@ module cv32e40x_wrapper
                               .prefetch_valid_if_i          (core_i.if_stage_i.prefetch_valid),
                               .prefetch_is_tbljmp_ptr_if_i  (core_i.if_stage_i.prefetch_is_tbljmp_ptr),
                               .*);
-  bind cv32e40x_cs_registers:        core_i.cs_registers_i              cv32e40x_cs_registers_sva  #(.SMCLIC(SMCLIC)) cs_registers_sva (.*);
+  bind cv32e40x_cs_registers:
+    core_i.cs_registers_i
+      cv32e40x_cs_registers_sva
+        #(.SMCLIC(SMCLIC))
+        cs_registers_sva (.wb_valid_i (core_i.wb_valid),
+                          .*);
 
   bind cv32e40x_load_store_unit:
     core_i.load_store_unit_i cv32e40x_load_store_unit_sva #(.DEPTH (DEPTH)) load_store_unit_sva (
@@ -263,11 +269,9 @@ module cv32e40x_wrapper
                 .branch_taken_in_ex               (core_i.controller_i.controller_fsm_i.branch_taken_ex),
                 .exc_cause                        (core_i.controller_i.controller_fsm_i.exc_cause),
                 // probed controller signals
-                .ctrl_fsm_ns                      (core_i.controller_i.controller_fsm_i.ctrl_fsm_ns),
                 .ctrl_debug_mode_n                (core_i.controller_i.controller_fsm_i.debug_mode_n),
                 .ctrl_pending_debug               (core_i.controller_i.controller_fsm_i.pending_debug),
                 .ctrl_debug_allowed               (core_i.controller_i.controller_fsm_i.debug_allowed),
-                .ctrl_pending_nmi                 (core_i.controller_i.controller_fsm_i.pending_nmi),
                 .ctrl_pending_interrupt           (core_i.controller_i.controller_fsm_i.pending_interrupt),
                 .ctrl_interrupt_allowed           (core_i.controller_i.controller_fsm_i.interrupt_allowed),
                 .id_stage_multi_cycle_id_stall    (core_i.id_stage_i.multi_cycle_id_stall),
@@ -283,9 +287,19 @@ module cv32e40x_wrapper
                 .irq_ack                          (core_i.irq_ack),
                 .mie_n                            (core_i.cs_registers_i.mie_n),
                 .mie_we                           (core_i.cs_registers_i.mie_we),
-                .clic_irq_q                       (core_i.gen_clic_interrupt.clic_int_controller_i.clic_irq_q),
-                .clic_irq_level_q                 (core_i.gen_clic_interrupt.clic_int_controller_i.clic_irq_level_q),
                 .*);
+generate
+if (SMCLIC) begin : clic_asserts
+  bind cv32e40x_clic_int_controller:
+    core_i.gen_clic_interrupt.clic_int_controller_i
+      cv32e40x_clic_int_controller_sva
+        clic_int_controller_sva (.ctrl_pending_interrupt  (core_i.controller_i.controller_fsm_i.pending_interrupt),
+                                 .ctrl_interrupt_allowed  (core_i.controller_i.controller_fsm_i.interrupt_allowed),
+                                 .ctrl_fsm                (core_i.ctrl_fsm),
+                                 .dcsr                    (core_i.dcsr),
+                                 .*);
+end
+endgenerate
 
   bind cv32e40x_sleep_unit:
     core_i.sleep_unit_i cv32e40x_sleep_unit_sva

rtl/cv32e40x_controller.sv

@@ -79,6 +79,7 @@ module cv32e40x_controller import cv32e40x_pkg::*;
   input  logic [1:0]  lsu_err_wb_i,               // LSU bus error in WB stage
   input  logic        lsu_busy_i,                 // LSU is busy with outstanding transfers
   input  logic        lsu_interruptible_i,        // LSU may be interrupted
+  input  logic        lsu_valid_wb_i,             // LSU is valid in WB (factors in rvalid from either OBI bus or write buffer)
 
   // jump/branch signals
   input  logic        branch_decision_ex_i,       // branch decision signal from EX ALU
@@ -182,6 +183,7 @@ module cv32e40x_controller import cv32e40x_pkg::*;
     .wb_valid_i                  ( wb_valid_i               ),
     .last_op_wb_i                ( last_op_wb_i             ),
     .abort_op_wb_i               ( abort_op_wb_i            ),
+    .lsu_valid_wb_i              ( lsu_valid_wb_i           ),
 
     .lsu_interruptible_i         ( lsu_interruptible_i      ),
 

rtl/cv32e40x_controller_bypass.sv

@@ -144,7 +144,12 @@ module cv32e40x_controller_bypass import cv32e40x_pkg::*;
   // This is needed because the data bypass from EX uses csr_rdata, and for mnxti this is actually mstatus and not the result
   // that will be written to the register file. Could be optimized to only stall when the result from the CSR instruction is used in ID,
   // but the common usecase is a CSR access followed by a branch using the mnxti result in the RF, so it would likely stall in most cases anyway.
-  assign ctrl_byp_o.mnxti_stall = csr_mnxti_read_i;
+  assign ctrl_byp_o.mnxti_stall_id = csr_mnxti_read_i;
+
+  // Stall EX stage when an mnxti is in EX and an LSU instruction is in WB.
+  // This is needed to make sure that any external interrupt clearing (due to a LSU instruction) gets picked
+  // up correctly by the mnxti access.
+  assign ctrl_byp_o.mnxti_stall_ex = csr_mnxti_read_i && (ex_wb_pipe_i.lsu_en && ex_wb_pipe_i.instr_valid);
 
   genvar i;
   generate

rtl/cv32e40x_controller_fsm.sv

@@ -75,6 +75,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
   // From LSU (WB)
   input  mpu_status_e lsu_mpu_status_wb_i,        // MPU status (WB timing)
   input  logic        data_stall_wb_i,            // WB stalled by LSU
+  input  logic        lsu_valid_wb_i,             // LSU instruction in WB is valid
 
   input  logic        lsu_busy_i,                 // LSU is busy with outstanding transfers
   input  logic        lsu_interruptible_i,        // LSU can be interrupted
@@ -228,6 +229,9 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
   logic       sequence_in_progress_id;
   logic       id_stage_haltable;
 
+  // Flag that is high during the cycle after an LSU instruction finishes in WB
+  logic       interrupt_blanking_q;
+
   assign sequence_interruptible = !sequence_in_progress_wb;
 
   assign id_stage_haltable = !sequence_in_progress_id;
@@ -440,10 +444,10 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
   // Once the first part of a table jump has finished in WB, we are not allowed to take interrupts before the last part finishes. This can be detected when the last
   // part of a table jump is in either EX or WB.
 
-  assign interrupt_allowed = lsu_interruptible_i && debug_interruptible && !fencei_ongoing && !xif_in_wb && sequence_interruptible;
+  assign interrupt_allowed = lsu_interruptible_i && debug_interruptible && !fencei_ongoing && !xif_in_wb && sequence_interruptible && !interrupt_blanking_q;
 
-  // Allowing NMI's follow the same rule as regular interrupts.
-  assign nmi_allowed = interrupt_allowed;
+  // Allowing NMI's follow the same rule as regular interrupts, except we don't need to regard blanking of NMIs after a load/store.
+  assign nmi_allowed = lsu_interruptible_i && debug_interruptible && !fencei_ongoing && !xif_in_wb && sequence_interruptible;
 
   // Do not allow interrupts if in debug mode, or single stepping without dcsr.stepie set.
   assign debug_interruptible = !(debug_mode_q || (dcsr_i.step && !dcsr_i.stepie));
@@ -521,7 +525,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
     //             Sequences:    If we need to halt for debug or interrupt not allowed due to a sequence, we must check if we can
     //                           actually halt the ID stage or not. Halting the same sequence that causes *_allowed to go to 0
     //                           may cause a deadlock.
-    ctrl_fsm_o.halt_id          = ctrl_byp_i.jalr_stall || ctrl_byp_i.load_stall || ctrl_byp_i.csr_stall || ctrl_byp_i.wfi_stall || ctrl_byp_i.mnxti_stall ||
+    ctrl_fsm_o.halt_id          = ctrl_byp_i.jalr_stall || ctrl_byp_i.load_stall || ctrl_byp_i.csr_stall || ctrl_byp_i.wfi_stall || ctrl_byp_i.mnxti_stall_id ||
       (((pending_interrupt && !interrupt_allowed) || (pending_nmi && !nmi_allowed) || (pending_nmi_early)) && debug_interruptible && id_stage_haltable) ||
       (pending_debug && !debug_allowed && id_stage_haltable);
 
@@ -530,7 +534,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
     // Also halting EX if an offloaded instruction in WB may cause an exception, such that a following offloaded
     // instruction can correctly receive commit_kill.
     // Halting EX when an instruction in WB may cause an interrupt to become pending.
-    ctrl_fsm_o.halt_ex          = ctrl_byp_i.minstret_stall || ctrl_byp_i.xif_exception_stall || ctrl_byp_i.irq_enable_stall;
+    ctrl_fsm_o.halt_ex          = ctrl_byp_i.minstret_stall || ctrl_byp_i.xif_exception_stall || ctrl_byp_i.irq_enable_stall || ctrl_byp_i.mnxti_stall_ex;
     ctrl_fsm_o.halt_wb          = 1'b0;
 
     // By default no stages are killed
@@ -1020,6 +1024,18 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
     end
   end
 
+  // Flop used to track LSU instructions in WB. High in the cycle after an LSU instruction
+  // leaves WB.
+  // Used for disregarding interrupts one cycle after a load/store to make sure the
+  // interrupt controller propagates the inputs through its flops.
+  always_ff @(posedge clk, negedge rst_n) begin
+    if (rst_n == 1'b0) begin
+      interrupt_blanking_q <= 1'b0;
+    end else begin
+      interrupt_blanking_q <= ex_wb_pipe_i.instr_valid && ex_wb_pipe_i.lsu_en && lsu_valid_wb_i;
+    end
+  end
+
   // Flops for fencei handshake request
   always_ff @(posedge clk, negedge rst_n) begin
     if (rst_n == 1'b0) begin

rtl/cv32e40x_core.sv

@@ -851,6 +851,7 @@ module cv32e40x_core import cv32e40x_pkg::*;
     .lsu_err_wb_i                   ( lsu_err_wb             ),
     .lsu_busy_i                     ( lsu_busy               ),
     .lsu_interruptible_i            ( lsu_interruptible      ),
+    .lsu_valid_wb_i                 ( lsu_valid_wb           ),
 
     // jump/branch control
     .branch_decision_ex_i           ( branch_decision_ex     ),

rtl/include/cv32e40x_pkg.sv

@@ -1204,7 +1204,8 @@ typedef struct packed {
   logic         load_stall;             // Stall due to load operation
   logic         csr_stall;
   logic         wfi_stall;
-  logic         mnxti_stall;            // Stall due to mnxti CSR access in EX
+  logic         mnxti_stall_id;         // Stall ID due to mnxti CSR access in EX
+  logic         mnxti_stall_ex;         // Stall EX due to LSU instruction in WB
   logic         minstret_stall;         // Stall due to minstret/h read in EX
   logic         deassert_we;            // Deassert write enable and special insn bits
   logic         id_stage_abort;         // Same signal as deassert_we, with better name for use in the controller.

sva/cv32e40x_clic_int_controller_sva.sv

@@ -0,0 +1,76 @@
+// Copyright 2022 Silicon Labs, Inc.
+//
+// This file, and derivatives thereof are licensed under the
+// Solderpad License, Version 2.0 (the "License").
+//
+// Use of this file means you agree to the terms and conditions
+// of the license and are in full compliance with the License.
+//
+// You may obtain a copy of the License at:
+//
+//     https://solderpad.org/licenses/SHL-2.0/
+//
+// Unless required by applicable law or agreed to in writing, software
+// and hardware implementations thereof distributed under the License
+// is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS
+// OF ANY KIND, EITHER EXPRESSED OR IMPLIED.
+//
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+////////////////////////////////////////////////////////////////////////////////
+// Engineer:       Øystein Knauserud - [email protected]           //
+//                                                                            //
+// Design Name:    cv32e40x_clic_int_controller_sva                           //
+// Project Name:   CV32E40X                                                   //
+// Language:       SystemVerilog                                              //
+//                                                                            //
+// Description:    Assertions reltated to the CLIC interrupt controller       //
+//                                                                            //
+////////////////////////////////////////////////////////////////////////////////
+
+module cv32e40x_clic_int_controller_sva
+  import uvm_pkg::*;
+  import cv32e40x_pkg::*;
+  (
+   input logic        clk,
+   input logic        rst_n,
+
+   input logic        irq_req_ctrl_o,
+   input logic        clic_irq_q,
+   input logic [7:0]  clic_irq_level_q,
+
+   input logic        ctrl_pending_interrupt,
+   input logic        ctrl_interrupt_allowed,
+
+   input ctrl_fsm_t   ctrl_fsm,
+   input dcsr_t       dcsr
+
+   );
+
+
+  // Check that a pending interrupt is taken as soon as possible after being enabled
+   property p_clic_enable;
+    @(posedge clk) disable iff (!rst_n)
+    ( !irq_req_ctrl_o
+       ##1
+       irq_req_ctrl_o && $stable(clic_irq_q) && $stable(clic_irq_level_q) && !(ctrl_fsm.debug_mode || (dcsr.step && !dcsr.stepie))
+       |-> (ctrl_pending_interrupt && ctrl_interrupt_allowed));
+  endproperty;
+
+  a_clic_enable: assert property(p_clic_enable)
+    else `uvm_error("core", "Interrupt not taken soon enough after enabling");
+
+  // Check a pending interrupt that is disabled is actually not taken
+  property p_clic_disable;
+    @(posedge clk) disable iff (!rst_n)
+    (  irq_req_ctrl_o
+        ##1
+        !irq_req_ctrl_o && $stable(clic_irq_q) && $stable(clic_irq_level_q)
+        |-> !(ctrl_pending_interrupt && ctrl_interrupt_allowed));
+  endproperty;
+
+  a_clic_disable: assert property(p_clic_disable)
+    else `uvm_error("core", "Interrupt taken after disabling");
+endmodule // cv32e40x_cs_registers_sva
+

sva/cv32e40x_core_sva.sv

@@ -72,24 +72,21 @@ module cv32e40x_core_sva
   input logic        data_req_o,
   input logic        data_we_o,
   input logic [5:0]  data_atop_o,
+  input logic        data_rvalid_i,
 
   // probed controller signals
   input logic        ctrl_debug_mode_n,
   input logic        ctrl_pending_debug,
   input logic        ctrl_debug_allowed,
   input logic        ctrl_interrupt_allowed,
   input logic        ctrl_pending_interrupt,
-  input              ctrl_state_e ctrl_fsm_ns,
   input ctrl_byp_t   ctrl_byp,
-  input logic        ctrl_pending_nmi,
-   // probed cs_registers signals
+  // probed cs_registers signals
   input logic [31:0] cs_registers_mie_q,
   input logic [31:0] cs_registers_mepc_n,
   input mcause_t     cs_registers_csr_cause_i, // From controller
   input mcause_t     cs_registers_mcause_q,    // From cs_registers, flopped mcause
-  input mstatus_t    cs_registers_mstatus_q,
-  input logic        clic_irq_q,
-  input logic [7:0]  clic_irq_level_q);
+  input mstatus_t    cs_registers_mstatus_q);
 
 if (SMCLIC) begin
   property p_clic_mie_tieoff;
@@ -484,31 +481,7 @@ end
   a_tbljmp_stall: assert property(p_tbljmp_stall)
     else `uvm_error("core", "Table jump not stalled while CSR is written");
 
-if (SMCLIC) begin
-    // Check that a pending interrupt is taken as soon as possible after being enabled
-  property p_clic_enable;
-    @(posedge clk) disable iff (!rst_ni)
-    ( !irq_req_ctrl
-       ##1
-       irq_req_ctrl && $stable(clic_irq_q) && $stable(clic_irq_level_q) && !(ctrl_fsm.debug_mode || (dcsr.step && !dcsr.stepie))
-       |-> (ctrl_pending_interrupt && ctrl_interrupt_allowed));
-  endproperty;
-
-  a_clic_enable: assert property(p_clic_enable)
-    else `uvm_error("core", "Interrupt not taken soon enough after enabling");
-
-  // Check a pending interrupt that is disabled is actually not taken
-  property p_clic_disable;
-    @(posedge clk) disable iff (!rst_ni)
-    (  irq_req_ctrl
-        ##1
-        !irq_req_ctrl && $stable(clic_irq_q) && $stable(clic_irq_level_q)
-        |-> !(ctrl_pending_interrupt && ctrl_interrupt_allowed));
-  endproperty;
-
-  a_clic_disable: assert property(p_clic_disable)
-    else `uvm_error("core", "Interrupt taken after disabling");
-end else begin
+if (!SMCLIC) begin
   // Check that a pending interrupt is taken as soon as possible after being enabled
   property p_mip_mie_write_enable;
     @(posedge clk) disable iff (!rst_ni)
@@ -533,5 +506,18 @@ end else begin
   a_mip_mie_write_disable: assert property(p_mip_mie_write_disable)
     else `uvm_error("core", "Interrupt taken after disabling");
 end
+
+// Clearing external interrupts via a store instruction causes irq_i to go low the next cycle.
+  // The interrupt controller uses flopped versions of irq_i, and thus we need to disregard interrupts
+  // for one cycle after an rvalid has been observed.
+property p_no_irq_after_lsu;
+  @(posedge clk) disable iff (!rst_ni)
+  (  wb_valid && ex_wb_pipe.lsu_en && ex_wb_pipe.instr_valid
+     |=>
+     !ctrl_interrupt_allowed);
+endproperty;
+
+a_no_irq_after_lsu: assert property(p_no_irq_after_lsu)
+  else `uvm_error("core", "Interrupt taken after disabling");
 endmodule // cv32e40x_core_sva
 

sva/cv32e40x_cs_registers_sva.sv

@@ -34,9 +34,17 @@ module cv32e40x_cs_registers_sva
    input logic        rst_n,
    input ctrl_fsm_t   ctrl_fsm_i,
    input id_ex_pipe_t id_ex_pipe_i,
+   input ex_wb_pipe_t ex_wb_pipe_i,
    input logic [31:0] csr_rdata_o,
    input logic        csr_we_int,
-   input logic [1:0]  mtvec_mode_o
+   input logic [1:0]  mtvec_mode_o,
+   input logic        wb_valid_i,
+   input logic        mnxti_we,
+   input logic        mintstatus_we,
+   input logic        mcause_we,
+   input logic [31:0] clic_pa_o,
+   input logic        clic_pa_valid_o
+
    );
 
 
@@ -53,6 +61,19 @@ module cv32e40x_cs_registers_sva
     assert property (@(posedge clk) disable iff (!rst_n)
                     1'b1 |-> mtvec_mode_o == 2'b11)
       else `uvm_error("cs_registers", "mtvec_mode is not 2'b11 in CLIC mode")
+
+  // Accesses to MNXTI are stalled in EX if there is a LSU instruction in WB.
+  // Thus no mnxti should be in WB (clic_pa_valid_o) the cycle after an LSU instruction
+  // is done in WB.
+  property p_no_mnxti_after_lsu;
+    @(posedge clk) disable iff (!rst_n)
+    (  wb_valid_i && ex_wb_pipe_i.lsu_en && ex_wb_pipe_i.instr_valid
+       |=>
+       !clic_pa_valid_o);
+  endproperty;
+
+  a_no_mnxti_after_lsu: assert property(p_no_mnxti_after_lsu)
+    else `uvm_error("core", "Mnxti should not we in WB the cycle after an LSU instruction");
   end
 endmodule // cv32e40x_cs_registers_sva