SVA for Finite State Machine

SystemVerilog
,
1

How can i write a assertion for finite state machine ?
Example : State A transits from A to State B when c = 1 or stays in State A as long as C =0 ;

2

State A transits from A to State B when c = 1 or stays in State A as long as C =0 ;

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) /// OK too

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
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; //

4

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

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)

6

In reply to kddholak:

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)

Why not? All signals in an assertion are sampled in the Preponed region (see 1800’2012 4.4 Stratified event scheduler), just before the clocking event.
state==A ##0 c is really equivalent to state==A && c; the difference is that

  1. state==A ##0 c |-> // means that if state==A is false, the attempt fails, and that thread is vacuous. there is no need to further evaluate the ##0 c, which means in same cycle c.
    2)state==A && c |-> the ANDing of those 2 expression is needed before determining success or failure for that attempt.
    Ben SystemVerilog.us