diff --git a/rtl/cv32e40x_clic_int_controller.sv b/rtl/cv32e40x_clic_int_controller.sv
index ac9a7e0c..6eea1577 100644
--- a/rtl/cv32e40x_clic_int_controller.sv
+++ b/rtl/cv32e40x_clic_int_controller.sv
@@ -122,6 +122,10 @@ module cv32e40x_clic_int_controller import cv32e40x_pkg::*;
   // and the incoming irq level is above the core's current effective interrupt level. Machine mode interrupts
   // during user mode shall always be taken if their level is > 0
 
+  // Cannot use flopped comparator results from the irq_wu_ctrl_o logic, as the effective_irq_level
+  // may change from one cycle to the next due to CSR updates. However, as the irq_wu_ctrl_o is only used
+  // when the core is in the SLEEP state (where no CSR updates can happen), an assertion exists to check that the cycle after a core wakes up
+  // due to an interupt the irq_req_ctrl_o must be asserted if global_irq_enable == 1;
   assign irq_req_ctrl_o = clic_irq_q && global_irq_enable &&
     ((priv_lvl_i == PRIV_LVL_M) ? (clic_irq_level_q > effective_irq_level) : (clic_irq_level_q > '0));
 
@@ -135,7 +139,6 @@ module cv32e40x_clic_int_controller import cv32e40x_pkg::*;
   // - priv mode == current, irq i is max (done in external CLIC), level > max(mintstatus.mil, mintthresh.th)
   // - priv mode  > current, irq i is max (done in external CLIC), level != 0
 
-  // todo: can we share the comparator below and flop the result for irq_req_ctrl_o?
   assign irq_wu_ctrl_o = clic_irq_i &&
     ((priv_lvl_i == PRIV_LVL_M) ? (clic_irq_level_i > effective_irq_level) : (clic_irq_level_i > '0));
 
diff --git a/sva/cv32e40x_clic_int_controller_sva.sv b/sva/cv32e40x_clic_int_controller_sva.sv
index b4cd0e22..a9a21438 100644
--- a/sva/cv32e40x_clic_int_controller_sva.sv
+++ b/sva/cv32e40x_clic_int_controller_sva.sv
@@ -40,6 +40,9 @@ module cv32e40x_clic_int_controller_sva
    input logic        clic_irq_q,
    input logic [7:0]  clic_irq_level_q,
 
+   input logic        global_irq_enable,
+   input logic        irq_wu_ctrl_o,
+
    input logic        ctrl_pending_interrupt,
    input logic        ctrl_interrupt_allowed,
    input logic        ctrl_pending_nmi,
@@ -60,7 +63,7 @@ module cv32e40x_clic_int_controller_sva
   endproperty;
 
   a_clic_enable: assert property(p_clic_enable)
-    else `uvm_error("core", "Interrupt not taken soon enough after enabling");
+    else `uvm_error("clic_int_controller", "Interrupt not taken soon enough after enabling");
 
   // Check that only NMI and external debug take presedence over interrupts after being enabled by mret or CSR writes
   property p_irq_pri;
@@ -76,7 +79,7 @@ module cv32e40x_clic_int_controller_sva
   endproperty;
 
   a_irq_pri: assert property(p_irq_pri)
-    else `uvm_error("core", "Interrupt not taken soon enough after enabling")
+    else `uvm_error("clic_int_controller", "Interrupt not taken soon enough after enabling")
 
   // Check a pending interrupt that is disabled is actually not taken
   property p_clic_disable;
@@ -88,7 +91,22 @@ module cv32e40x_clic_int_controller_sva
   endproperty;
 
   a_clic_disable: assert property(p_clic_disable)
-    else `uvm_error("core", "Interrupt taken after disabling");
+    else `uvm_error("clic_int_controller", "Interrupt taken after disabling");
+
+  // If an interrupt wakeup is signalled while the core is in the SLEEP state, an interrupt
+  // request must be asserted in the next cycle if the signal global_irq_enable is set.
+  property p_req_after_wake;
+    @(posedge clk) disable iff (!rst_n)
+    (  (ctrl_fsm_cs == SLEEP) &&  // Core is in sleep state
+       irq_wu_ctrl_o              // Wakeup requested
+       |=>
+       (irq_req_ctrl_o) // interrupts must be requested
+       or
+       (!irq_req_ctrl_o && !global_irq_enable)); // unless interrupts are not enabled
+  endproperty;
+
+  a_req_after_wake: assert property(p_req_after_wake)
+    else `uvm_error("clic_int_controller", "No request after wakeup signal");
 
 endmodule
 
diff --git a/sva/cv32e40x_core_sva.sv b/sva/cv32e40x_core_sva.sv
index e059d49c..c0f56854 100644
--- a/sva/cv32e40x_core_sva.sv
+++ b/sva/cv32e40x_core_sva.sv
@@ -55,6 +55,7 @@ module cv32e40x_core_sva
   input logic        irq_ack, // irq ack output
   input logic        irq_clic_shv, // ack'ed irq is a CLIC SHV
   input logic        irq_req_ctrl, // Interrupt controller request an interrupt
+  input logic        irq_wu_ctrl,
   input ex_wb_pipe_t ex_wb_pipe,
   input logic        wb_valid,
   input logic        branch_taken_in_ex,
@@ -131,7 +132,8 @@ module cv32e40x_core_sva
   input logic [1:0]  lsu_cnt_q,
   input logic [1:0]  resp_filter_bus_cnt_q,
   input logic [1:0]  resp_filter_core_cnt_q,
-  input write_buffer_state_e write_buffer_state
+  input write_buffer_state_e write_buffer_state,
+  input privlvl_t    priv_lvl
 );
 
 if (CLIC) begin
@@ -690,6 +692,21 @@ if (!CLIC) begin
 
   a_mip_mie_write_disable: assert property(p_mip_mie_write_disable)
     else `uvm_error("core", "Interrupt taken after disabling");
+
+  // If an interrupt wakeup is signalled while the core is in the SLEEP state, an interrupt
+  // request must be asserted in the next cycle if interrupts are globally enabled.
+  property p_req_after_wake;
+    @(posedge clk) disable iff (!rst_ni)
+    (  (ctrl_fsm_cs == SLEEP) &&  // Core is in sleep state
+        irq_wu_ctrl               // Wakeup requested
+        |=>
+        (irq_req_ctrl)  // interrupt must be requested
+        or
+        (!irq_req_ctrl && !(cs_registers_mstatus_q.mie || (priv_lvl < PRIV_LVL_M)))); // unless interrupts are disabled
+  endproperty;
+
+  a_req_after_wake: assert property(p_req_after_wake)
+    else `uvm_error("core", "No interrupt request after wakeup signal");
 end
 
 // Clearing external interrupts via a store instruction causes irq_i to go low the next cycle.