SVA Multiple FSM States

Hello SVA Experts,

The design state machine is having lets say 4 states, S1, S2, S3 and S4.
From S1 I can reach S2, S3 or S4 (Only 1 of them shall be True at any given time)
S1 to S2 is single clk cycle state transition.
S1 to S3/S4 may be multiple clock Cycles (this can vary).

I have coded initially as below.

property S1_2_S2_S3_S4_CHECKS; 
  @(posedge clks) disable iff(~POR_N)
  (state === S1) |=> (state === S2) || (state === S3) || (state === S4); 
endproperty

option1: This passes for all cases.

(state === S1) |->##[1:$] (state === S2) || (state === S3) || (state === S4); 

option2 :

first_match((state === S1) |->##[1:$] (state === S2) || (state === S3) || (state === S4));

Please suggest if these options are right to use.

Also there is a very common requirement that when reset is applied, there is a default state say S1 in the above case. As there is no clock involved how do we write an assertion for this?

Thanks

In reply to raviji:
You need to use the sequential or operator.


property S1_2_S2_S3_S4_CHECKS; 
      @(posedge clks) disable iff(!POR_N)
      state === S1 |=> state === S2 or 
                       ##[0:$] (state === S3) || (state === S4); 
endproperty

ap_reset2s1: assert property(@ (posedge clk)  // synchronous 
      !POR_N |=> state === S1); 

always_comb if(!POR_N) state === S1; // asynchronous 
  

NOTES

  1. There is NO need for a first_match() in an antecendent when there is only ONE thread
    first_match((state === S1) |-> // NO TO THIS!!!
  2. On logical operations use the logical operators. Thus,
    !POR_N // YES TO THIS
    ~POR_N // NOT recommended, as it implies that POR_N is a vector> 1bit

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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 978-1539769712
  • 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

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
  4. FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy

In reply to ben@SystemVerilog.us:

Hi Ben, Raviji,
This assertion will not fail if the state transition does not take place from S1 to any of the states because of ##[0:$]. It appears like the only time the assertion fails if the transition from S1 to S2 takes more than 1 clock cycle. Please correct me if I am wrong.

In reply to ManjunathBhat:
You would need the strong operator


state === S1 |=> strong (state === S2 or 
                       ##[0:$] (state === S3) || (state === S4)); 

In reply to ben@SystemVerilog.us:

In reply to ManjunathBhat:
You would need the strong operator


state === S1 |=> strong (state === S2 or 
##[0:$] (state === S3) || (state === S4)); 

Thanks Ben.