Controller_fsm cleanup and asserts

rtl/cv32e40x_controller_fsm.sv

@@ -434,7 +434,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
   assign single_step_allowed = 1'b1;
 
   /*
-  Debug spec 1.0.0 (unratified as of Aug 9th '21)
   "If control is transferred to a trap handler while executing the instruction, then Debug Mode is
   re-entered immediately after the PC is changed to the trap handler, and the appropriate tval and
   cause registers are updated. In this case none of the trap handler is executed, and if the cause was
@@ -1189,7 +1188,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
   end
 
   // Wakeup from sleep
-  assign ctrl_fsm_o.wake_from_sleep = pending_nmi || irq_wu_ctrl_i || pending_async_debug || debug_mode_q || (wfe_in_wb && wu_wfe_i); // Only WFE wakes up for wfe_wu_i
+  assign ctrl_fsm_o.wake_from_sleep = pending_nmi || irq_wu_ctrl_i || pending_async_debug || (wfe_in_wb && wu_wfe_i); // Only WFE wakes up for wfe_wu_i
   assign ctrl_fsm_o.debug_no_sleep = debug_mode_q || dcsr_i.step;
 
   ////////////////////

sva/cv32e40x_controller_fsm_sva.sv

@@ -135,7 +135,8 @@ module cv32e40x_controller_fsm_sva
   input logic           mret_ptr_in_id,
   input logic           alu_jmpr_id_i,
   input logic [31:0]    jalr_fw_id_i,
-  input logic [REGFILE_WORD_WIDTH-1:0] rf_mem_i [(RV32 == RV32I) ? 32 : 16]
+  input logic [REGFILE_WORD_WIDTH-1:0] rf_mem_i [(RV32 == RV32I) ? 32 : 16],
+  input logic           non_shv_irq_ack
 );
 
 
@@ -1128,6 +1129,24 @@ generate
                         etrigger_in_wb |-> exception_in_wb)
         else `uvm_error("controller", "etrigger_in_wb when there is no exception in WB")
 
+    a_no_etrig_on_halt_or_kill:
+      assert property (@(posedge clk) disable iff (!rst_n)
+                        (ctrl_fsm_o.halt_wb || ctrl_fsm_o.kill_wb)
+                        |->
+                        !etrigger_in_wb)
+        else `uvm_error("controller", "etrigger_in_wb when WB is halted or killed")
+
+    a_no_step_on_halt_or_kill:
+      assert property (@(posedge clk) disable iff (!rst_n)
+                        (ctrl_fsm_o.halt_wb || ctrl_fsm_o.kill_wb) // WB is halted or killed
+                        |->
+                        !pending_single_step                       // No single step should be pending
+                        or
+                        non_shv_irq_ack                            // Unless we ack an non-shv interrupt (kills WB)
+                        or
+                        (pending_nmi && nmi_allowed))              // or we take an NMI (kills WB)
+        else `uvm_error("controller", "pending single step when WB is halted or killed")
+
      // Only halt LSU instruction in WB for watchpoint trigger matches
     a_halt_lsu_wb:
       assert property (@(posedge clk) disable iff (!rst_n)
@@ -1191,6 +1210,13 @@ generate
                       (debug_cause_q == DBG_CAUSE_STEP))
         else `uvm_error("controller", "Wrong debug cause when taking an interrupt during single stepping")
 
+    a_no_sleep_during_debug:
+      assert property (@(posedge clk) disable iff (!rst_n)
+                      (ctrl_fsm_cs == SLEEP)
+                      |->
+                      !debug_mode_q)
+      else `uvm_error("controller", "Debug mode during SLEEP not allowed")
+
 if (CLIC) begin
     // While single stepping, debug cause shall be set to 'trigger' if a pointer for a SHV CLIC interrupt arrives in WB
     // with an exception and an exception trigger that matches the exception has been configured. (trigger > step)