In reply to ben@SystemVerilog.us:
Thank you for answering for my Queries.
I tried for few above listed Queries, Please correct it when assertions are went wrong
-
Every sig_a must eventually be acknowledged by sig_b, unless sig_c appears.
sig_a|=> !sig_c ##1 sig_b -
if the state machine reaches state=ACTIVE1, it will eventually reach state=ACTIVE2.
state==ACTIVE1 |-> 1[0:$] ##1 state==ACTIVE2 -
sig_a must not rise if we have seen sig_b and havent seen the next sig_c yet(from the cycle after the sig_b until the cycle before the sig_c)
!sig_a |=> sig_b[0:$] ##1 sig_a |=> sig_c -
if sig_a is down , sig_b may only rise for one cycle before the next time that sig_a is asserted.
!sig_a |-> 1[0:$] ##1 sig_b |=> sig_a -
The Auxiliary signal sig_a indicates that we have seen a sig_b, and havent seen a sig_C since then. it rises one cycle after the sig_b, and falls one cycle after the sig_c.
sig_a |=> (sig_b and !sig_c) ##1 sig_c ##1 !sig_b