SVA for Finite State Machine

SystemVerilog
,
3

In reply to ben@SystemVerilog.us:

Thanks ben for the answer.
What if I do this way instead what you have proposed. Is it the right way to check FSM ?

ap_A2B: assert property(@(posedge clk)
state==b && c |-> $past(state)==A;
ap_A2B: assert property(@(posedge clk)
$past(state)==A && !c |-> state==A; //