[alert,fpv] Add stopats and assertions to hit parasitic FSM states

Signed-off-by: Rupert Swarbrick <[email protected]>

Author: rswarbrick

hw/ip/prim/fpv/tb/rxtx_after_load.tcl

@@ -5,7 +5,32 @@
 # This is a TCL file that can be sourced by FPV runs that are doing
 # some form of "prim_alert_rxtx" verification.
 
+proc move_to_task {task_name assert_name} {
+    task -edit ${task_name} -copy "${assert_name}*"
+    assert -disable ${assert_name}
+}
+
+
 set valid_state_props [get_property_list -regexp -include {"name" "ValidState_A$"}]
 foreach prop $valid_state_props {
     assert -set_helper $prop
 }
+
+# The property names in this list are properties that depend on some FSM state register pointing at
+# a parasitic state. Use a stopat on various state registers to make the properties say something.
+
+task -create FreeFsm
+stopat -task FreeFsm "i_prim_alert_sender.state_q"
+stopat -task FreeFsm "i_prim_alert_receiver.state_q"
+
+set parasitic_state_props {SenderStateDValid_A ReceiverStateDValid_A}
+
+foreach psn $parasitic_state_props {
+    foreach psp [get_property_list -regexp -include [list name "${psn}$"]] {
+        move_to_task FreeFsm $psp
+    }
+}
+
+# Add FreeFsm to the cov_tasks variable, which is a list of the tasks that will be used for
+# check_cov at the end of fpv.tcl if coverage is enabled.
+lappend cov_tasks FreeFsm

hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert_fpv.sv

@@ -221,4 +221,29 @@ module prim_alert_rxtx_async_assert_fpv
       ##[1:30] sender_is_idle,
       clk_i, !rst_ni || error_present)
 
+  // There is a single parasitic state in the FSM of prim_alert_sender (because state_e uses 3 bits
+  // to define 7 states). The sender rather sensibly uses state_d to get back to Idle in that case
+  // as an escape route. Using a stopat to check this is fiddly because then state_d won't *have*
+  // any effect. To make this work, assert that state_d is a known state. This shows that the escape
+  // route has been wired up correctly.
+  SenderStateDValid_A: assert property (i_prim_alert_sender.state_d inside
+                                        { i_prim_alert_sender.Idle,
+                                          i_prim_alert_sender.AlertHsPhase1,
+                                          i_prim_alert_sender.AlertHsPhase2,
+                                          i_prim_alert_sender.PingHsPhase1,
+                                          i_prim_alert_sender.PingHsPhase2,
+                                          i_prim_alert_sender.Pause0,
+                                          i_prim_alert_sender.Pause1 });
+
+  // As with the previous assertion, there are two parasitic states in the FSM of
+  // prim_alert_receiver (state_e uses 3 bits to define 6 states). Again, assert that state_d is a
+  // known state.
+  ReceiverStateDValid_A: assert property (i_prim_alert_receiver.state_d inside
+                                          { i_prim_alert_receiver.Idle,
+                                            i_prim_alert_receiver.HsAckWait,
+                                            i_prim_alert_receiver.Pause0,
+                                            i_prim_alert_receiver.Pause1,
+                                            i_prim_alert_receiver.InitReq,
+                                            i_prim_alert_receiver.InitAckWait });
+
 endmodule : prim_alert_rxtx_async_assert_fpv