How to include internal state of FSM in SV Assertion?

SystemVerilog
, ,
1

I want to write SV Assertion for a FSM is a separate file.
I have defined the states as reg in my rtl file.
How can i write assertion for FSM state.

For example if i have 4 states s1,s2,s3 and s4 in my FSM.

Along with input signals in Assertion files how can i include states.

2

In reply to nayan2208:

I want to write SV Assertion for a FSM is a separate file.
I have defined the states as reg in my rtl file.
How can i write assertion for FSM state.
For example if i have 4 states s1,s2,s3 and s4 in my FSM.
Along with input signals in Assertion files how can i include states.

Several comments on this topic:

  1. Assertions can be written in a separate module or checker and be bound to the DUT, or instantiated statically or procedurally (for checkers only).
  2. When writing assertions for FSMs, you should NOT emulate in the assertion the FSM code. For example, the following IS NOT recommended

// Very BAD assertion style
typedef enum {ST0, ST1, ST2, ST3 } fsm_e; // ch2/2.6/types.sv
fsm_e state;
ap: assert property( // using the default clocking
case (state)
ST0 :  a |=> state==ST1;
ST1 :  if(b) ##1 state=ST2
else  ##1 ststa=ST1
ST3 : ...
default: 0;
endcase
);

The reason this style of assertion is poor is because it mimic RTL and does no real verification
3. A better style in approaching the sequence of states is to use a higher approach; by that, I mean using more of the eventualities and general relationships between states.
For example, considering traffic light controller as a simple example, where, instead of defining the transition between states, I define the relationships. The follow pages are extracted from my book SystemVerilog Assertions Handbook, 4th Edition
Cohen book: FSM assertions (pdf file)
You should also add coverage.

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

  • 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 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

Hi Ben,

“Case-statement inside SVA is not supported”
I got above error when I used case statement in property.

-Vivek

4

In reply to Vivek Kumar Rai:

“Case-statement inside SVA is not supported”
I got above error when I used case statement in property.

The caseproperty statement is part of SVA; however, the lack of support by some vendors is a tool issue. As an alternative, you can use the if else statement or just multiple smaller assertions. For example:


 ap_with_if: assert property(
    if(bus_select==2'b01) $rose(req1)|-> ##[1:5] ack1 else 
    if(bus_select==2'b10) $rose(req2)|-> ##[1:5] ack2);  
    
  ap_1: assert property(
    (bus_select==2'b01) && $rose(req1)|-> ##[1:5] ack1); 
      
  ap_2: assert property(
    (bus_select==2'b10) && $rose(req2)|-> ##[1:5] ack2);

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