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:
Assertions can be written in a separate module or checker and be bound to the DUT, or instantiated statically or procedurally (for checkers only).
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.
“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: