[dv/pwrmgr] Fix assertion for usb_clk_en_active
Compare usb_clk_en against the captured value of usb_clk_en_active_i
since the latter value can change anytime.
Signed-off-by: Guillermo Maturana <maturana@google.com>
diff --git a/hw/ip/pwrmgr/dv/sva/pwrmgr_clock_enables_if.sv b/hw/ip/pwrmgr/dv/sva/pwrmgr_clock_enables_if.sv
index dc7b0c8..9d3d8c8 100644
--- a/hw/ip/pwrmgr/dv/sva/pwrmgr_clock_enables_if.sv
+++ b/hw/ip/pwrmgr/dv/sva/pwrmgr_clock_enables_if.sv
@@ -31,15 +31,21 @@
sequence transitionDown_S; state == pwrmgr_pkg::SlowPwrStatePwrClampOn; endsequence
+ sequence usbActiveTransition_S;
+ logic prev_en;
+ (1'b1, prev_en = usb_clk_en_active_i) ##1 usb_clk_en == prev_en;
+ endsequence
+
`ASSERT(CoreClkPwrUp_A, transitionUp_S |=> core_clk_en == 1'b1, clk_i, reset_or_disable)
`ASSERT(IoClkPwrUp_A, transitionUp_S |=> io_clk_en == 1'b1, clk_i, reset_or_disable)
`ASSERT(UsbClkPwrUp_A, transitionUp_S |=> usb_clk_en == usb_clk_en_active_i, clk_i,
reset_or_disable)
+ // This deals with transitions while the fast fsm is active.
`ASSERT(UsbClkActive_A,
state == pwrmgr_pkg::SlowPwrStateIdle && $changed(
usb_clk_en_active_i
- ) |=> usb_clk_en == usb_clk_en_active_i,
+ ) |-> usbActiveTransition_S,
clk_i, reset_or_disable)
`ASSERT(CoreClkPwrDown_A, transitionDown_S |=> core_clk_en == core_clk_en_i, clk_i,
