How do we write assumptions into a Formal Setup to create sequence which has to hit mandatorily

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
           }) );

This Siemens sponsored public forum is not for discussing tool specific issues. Please read your tool’s User Manual or contact your tool vendor for support.