I’m working on a Formal for LiveLock & Deadlock. I’m using FORMAL TOOL for the same. I’m noticing none of my sequence assumption is getting picked up by the tool.
Here’s the desired sequence:e@ to trigger FSM. (i’m trying to remove/ avoid illegal values to get FSM going). I want formal engine to always drive the initial_trigger_sequence first to avoid invalid deadlocks then get into the values mentioned in the set {}. But it’s not picking up.
// 'h14231 (PAVP_SESSION) -> 'KEY_PAVP_0 -> 'KEY_PAVP_1 -> 'h14234 (PAVP_CONREQ)
// Initial sequence tracking
sequence initial_trigger_sequence;
client_pavp.dwaddr == 'h14231 and // PAVP_SESSION
// Wait for first fall edge of signal_ready
($fell(client_pavp.ready) ##2 client_pavp.dwaddr inside {'h14200, 'h14201, 'h14202, 'h14203}) and // KEY_PAVP_0
// Next address transition after another signal_ready fall
($fell(client_pavp.ready) ##2 client_pavp.dwaddr inside {'h14204, 'h14205, 'h14206, 'h14207}) and // KEY_PAVP_1
// Final address transition- PAVP_CONREQ
($fell(client_pavp.ready) ##2 client_pavp.dwaddr == 'h14234); endsequence
// Track the progression of addresses after signal_ready falls
rmbus_addr_assumption: assume property (
@(posedge cdclk) disable iff (!par0_de_cdrst_b)
(
initial_trigger_sequence |-> // PAVP_CONREQ
client_pavp.dwaddr inside {
'h21600,
'h14210, 'h14211, 'h14212, 'h14213,
'h14214, 'h14215, 'h14216, 'h14217,
'h14231,
'h14100
}) );