Fix for issue #499.

rtl/cv32e40x_cs_registers.sv

@@ -970,10 +970,18 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*;
             // mpil is saved from mintstatus
             mcause_n.mpil = mintstatus_rdata.mil;
 
-            // todo: handle exception vs interrupt
             // Save new interrupt level to mintstatus
-            mintstatus_n.mil = ctrl_fsm_i.irq_level;
-            mintstatus_we = 1'b1;
+            // Horizontal synchronous exception traps do not change the interrupt level.
+            // Vertical synchronous exception traps to higher privilege level use interrupt level 0.
+            // All exceptions are taken in PRIV_LVL_M, so checking that we get a different privilege level is sufficient for clearing
+            // mintstatus.mil.
+            if (ctrl_fsm_i.csr_cause.irq) begin
+              mintstatus_n.mil = ctrl_fsm_i.irq_level;
+              mintstatus_we = 1'b1;
+            end else if ((priv_lvl_rdata != priv_lvl_n)) begin
+              mintstatus_n.mil = '0;
+              mintstatus_we = 1'b1;
+            end
           end else begin
             mcause_n.mpil = '0;
           end

sva/cv32e40x_cs_registers_sva.sv

@@ -43,7 +43,10 @@ module cv32e40x_cs_registers_sva
    input logic        mintstatus_we,
    input logic        mcause_we,
    input logic [31:0] clic_pa_o,
-   input logic        clic_pa_valid_o
+   input logic        clic_pa_valid_o,
+   input mintstatus_t mintstatus_rdata,
+   input privlvl_t    priv_lvl_n,
+   input privlvl_t    priv_lvl_rdata
 
    );
 
@@ -62,18 +65,31 @@ module cv32e40x_cs_registers_sva
                     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;
+    // 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");
+    a_no_mnxti_after_lsu: assert property(p_no_mnxti_after_lsu)
+      else `uvm_error("cs_registers", "Mnxti should not we in WB the cycle after an LSU instruction");
+
+
+    // Check that horizontal traps keep the current interrupt level
+    property p_htrap_interrupt_level;
+      @(posedge clk) disable iff (!rst_n)
+      (  ctrl_fsm_i.csr_save_cause && !ctrl_fsm_i.debug_csr_save && !ctrl_fsm_i.csr_cause.irq && (priv_lvl_n == priv_lvl_rdata)
+         |=>
+         $stable(mintstatus_rdata.mil));
+
+    endproperty;
+
+    a_htrap_interrupt_level: assert property(p_htrap_interrupt_level)
+      else `uvm_error("cs_registers", "Horizontal trap taken caused interrupt level to change");
   end
-endmodule // cv32e40x_cs_registers_sva
+endmodule