In reply to kddholak:
That would work. the two are somewhat diferent in meaning.
state==B && c |-> $past(state)==A; means that if you’re in state B and you have a c, it’s because you were in state A. However, if the fsm is complex, there may be another path that caused you to be in state B, and then you get a c in same cycle. Thus,
X |-> $past(Y) means that if in X, its because you were in Y. In complex FSMs, i may see
X |-> $past(Y) or $past(Z), i.e., different possible causes that led you to that condition X.
state==A ##0 c |=> state==B); means
if in A with a c then you must go to B. This is forward looking.
It all depends as to what you want to do or mean.
Note that when writing assertions fo FSM, don’t copy the code. Try to see the machne from a higher level, maybe skipping the intermediate states, and cover the key ones. For example, for a traffic light controller, If the North-South light just turned green (fsm_NS==GREEN)it because sometime before the sensor detected a car waiting, or because the timeout counter timed out.
Ben SystemVerilog.us