diff --git a/rtl/cv32e40x_controller_fsm.sv b/rtl/cv32e40x_controller_fsm.sv
index 63d94402..b8722c4f 100644
--- a/rtl/cv32e40x_controller_fsm.sv
+++ b/rtl/cv32e40x_controller_fsm.sv
@@ -1102,7 +1102,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
   end
 
   // Wakeup from sleep
-  assign ctrl_fsm_o.wake_from_sleep        = 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 || debug_mode_q || (wfe_in_wb && wu_wfe_i); // Only WFE wakes up for wfe_wu_i
   assign ctrl_fsm_o.debug_wfi_wfe_no_sleep = debug_mode_q || dcsr_i.step;
 
   ////////////////////
diff --git a/sva/cv32e40x_controller_fsm_sva.sv b/sva/cv32e40x_controller_fsm_sva.sv
index 8aae0103..ffa584f9 100644
--- a/sva/cv32e40x_controller_fsm_sva.sv
+++ b/sva/cv32e40x_controller_fsm_sva.sv
@@ -482,17 +482,17 @@ endgenerate
   a_no_wfi_wakeup_on_wfe:
   assert property (@(posedge clk) disable iff (!rst_n)
                     (ctrl_fsm_cs == SLEEP) && ex_wb_pipe_i.instr_valid && ex_wb_pipe_i.sys_en && ex_wb_pipe_i.sys_wfi_insn &&
-                    !irq_wu_ctrl_i && wu_wfe_i && !pending_async_debug
+                    !(irq_wu_ctrl_i || pending_nmi) && wu_wfe_i && !pending_async_debug
                     |=>
                     (ctrl_fsm_cs == SLEEP))
     else `uvm_error("controller", "WFI instruction woke up to wu_wfe_i")
 
-  // WFE wakes up to either interrupts or wu_wfe_i
+  // WFE wakes up to either interrupts (including NMI) or wu_wfe_i
   // Disregarding debug related reasons to wake up
   a_wfe_wakeup:
   assert property (@(posedge clk) disable iff (!rst_n)
                     (ctrl_fsm_cs == SLEEP) && ex_wb_pipe_i.instr_valid && ex_wb_pipe_i.sys_en && ex_wb_pipe_i.sys_wfe_insn &&
-                    (irq_wu_ctrl_i || wu_wfe_i) && !pending_async_debug
+                    (irq_wu_ctrl_i || wu_wfe_i || pending_nmi) && !pending_async_debug
                     |->
                     (ctrl_fsm_ns == FUNCTIONAL))
     else `uvm_error("controller", "WFE must wake up to interuppts or wu_wfe_i")