stanford
Full Member level 2
I have an assertion that says when you are in STATE1, after some time, it should to go STATE2.
How are the two assertion statements different? What's the best way to write an assertion to check that a state machine goes from state1 to state2?
((state == STATE1) ##[1:10] goto_state1_to_state2) |=> ##[0:6] (state == STATE2);
((state == STATE1) |=> ##[1:10] goto_state1_to_state2) |=> ##[0:6] (state == STATE2);
How are the two assertion statements different? What's the best way to write an assertion to check that a state machine goes from state1 to state2?
((state == STATE1) ##[1:10] goto_state1_to_state2) |=> ##[0:6] (state == STATE2);
((state == STATE1) |=> ##[1:10] goto_state1_to_state2) |=> ##[0:6] (state == STATE2);