SVA for Finite State Machine

SystemVerilog
,
5

In reply to ben@SystemVerilog.us:

I have noticed one thing. In above assertion.
// comment :
In below assertion if the signal C transition and state transition happen at the same time then it wont work ? Please correct if i am wrong.

ap_A2B: assert property(@(posedge clk)
state==A ##0 c |=> state==B);
ap_A2B: assert property(@(posedge clk)
state==A ##0 !c |=> state==A); // |=> $stable(state)