SVA for Invalid FSM state transition

LFT · January 12, 2024, 6:50pm

Hi Forum,
The intention of my SVA is to flag an error when the state machine transitions from S1 → S3 → S6.
The assertion should also consider cases that a state is stable across multiple clocks

Here is my attempt : edalink
‘ap2’ uses the same clocking event as fsm and throws an error on next clock of the NBA assignment of S6 ( since pre-poned values are used in concurrent assertions ) whereas ‘ap1’ uses SV regions to throw an error on same clock that the NBA assignment occurs.
I was trying to compare the advantages and disadvantages of both solution.
Here are a few advantages I have noted of ‘ap1’ over ‘ap2’

If there is no posedge of clock after T:65 , ‘ap2’ would never trigger the fail action block whereas ‘ap1’ would trigger it.
As the clocking event for ‘ap1’ is whenever ‘ps’ state changes, I believe it is more simulation efficient than ‘ap2’

I have a few questions for the forum moderators

[Q1] Are there any advantages of ‘ap2’ over ‘ap1’ ?
[Q2] Are there any disadvantages of ‘ap1’ ?
[Q3] Are both solution acceptable ?
[Q4] Are the solution an example of a valid use case of using multiple non-overlapping implication operators ? For other state transitions there would be a vacuous pass due to multiple |=> which I believe is fine as per intention

ben2 · January 12, 2024, 10:07pm

Use the system clock for the assertion.
I would NOT use a signal as a clock; it is bad practice. That style may not be supported by FV.
In general, I do not like these of multiple implication operators.
( ps == S1 ) |=> ( ps != S1 )[->1] ##0( ps == S3 )
DO you want the $rose(ps==S1)?
Why the ( ps != S1 )[->1] ?
Why not using ( ps == S3 [->1])?
I don’t like the not( ( ps != S3 )[->1] ##0 (ps == S6) );
because it does not express what the property should do.
How about something like:

property prop_better;    
    @(posedge clk)  // Clocking event on each posedge of clock
    ( ps == S1 ) |=> ( ps == S3 )[->1] ##1 
    (ps != S3 && ps!=S6)[->1] intersect  (ps != S6)[*1:$] ;  
  endproperty

Your TB should use nonblocking assignments as a good practice rule.
Aside from directed tests, you should consider randomization.
I strongly suggest that you read my reply on “Getting started with verification with SystemVerilog”
https://rb.gy/f3zhh
file is also attached.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
https://systemveri

roadmaptosva.pdf (172.0 KB)

LFT · January 13, 2024, 6:35pm

Hi Ben,
Please find attached comments

Use the system clock for the assertion.

If there is no clocking event after T:65 i.e on the posedge that ‘ns’ is assigned S6 there would be no error. Any way to bypass this limitation ?

DO you want the $rose(ps==S1) ?

Yes, this would be better to restrict the attempts

Why the ( ps != S1 )[->1] ?

Assume the sampled states on each posedge of clock are S1 , S1 , S1 , S3 , S3 , S3 , S3 , S6
So using ( ps != S1 ][->1] it waits for state to transition from S1 to non-S1 state thereby ignoring the same state S1 across multiple clocks.

Why not using ( ps == S3 )[->1])?

Using this I would observe assertion failure if the sampled states were S1 , S1 , S2 , S3 , S3 , S3 , S6.
Via ( ps != S1 )[->1] ## 0( ps == S3 ) , ‘ap2’ checks that after S1 the next non-S1 state is S3. So for above state transition there would be a vacuous pass due to transition to S2.

I don’t like the not( ( ps != S3 )[->1] ## 0 (ps == S6) );

Go-to repetition would wait for the non-S3 state after S3. If the non-S3 state is S6 the assertion fails as per intention

A few questions of mine ::

In general, I do not like these of multiple implication operators.

An alternative I tried edalink2 .
(a) Would like to hear your thoughts on it

In general, I do not like these of multiple implication operators.

(b) This particular question was the 1st case that I thought could use multiple non-overlapping implication.

If the sample states over posedge of clock is S1 , S1 , S2 there would be a vacuous pass due to 2nd |=>

ben2 · January 13, 2024, 8:36pm

[Ben_Q] Why the ( ps != S1 )[->1] ?

[UR_A] Assume the sampled states on each posedge of clock are S1 , S1 , S1 , S3 , S3 , S3 , S3 , S6
So using ( ps != S1 ][->1] it state thereby ignoring the same state S1 across multiple clocks.

[Ben_A] ( ps != S1 ][->1] is same as !(ps!=S1)[*0:$] ##1 ps!=S1

YES on “waits for state to transition from S1 to non-S1”.

NO on “ignoring the same state S1 across multiple clocks.”

[Ben_Q] Why not using ( ps == S3 )[->1])?

[UR_A] Using this I would observe assertion failure if the sampled states were S1 , S1 , S2 , S3 , S3 , S3 , S6.
Via ( ps != S1 )[->1] ## 0( ps == S3 ) , ‘ap2’ checks that after S1 the next non-S1 state is S3. So for above state transition there would be a vacuous pass due to transition to S2.

[Ben_A] I generally do not recommend the verification of FSM with assertions between states. FSMs should be verified thru assertions of the requirements. For example,
$rose(tlight==YELLOW) |=> tlight==YELLOW[*1:4] ##1 tlight == RED;

[Ben_Q] I don’t like the not( ( ps != S3 )[->1] ## 0 (ps == S6) );

[UR_A] Go-to repetition would wait for the non-S3 state after S3. If the non-S3 state is S6 the assertion fails as per intention

[Ben_A] As a matter of preference, I prefer to write assertions that define what SHOULD be true instead of what should NOT be true. I sometimes use the “not” operator, but not too often.

[UR_Q] A few questions of mine ::In general, I do not like these of multiple implication operators.

An alternative I tried edalink2 .
(a) Would like to hear your thoughts on it

In general, I do not like these of multiple implication operators.

[Ben_A] With nultiple implication operators you have multiple cases of vacuity; it makes the assertion more complex IMHO.
I prefer multiple simple assertions over complex ones.

(b) This particular question was the 1st case that I thought could use multiple non-overlapping implication.

If the sample states over posedge of clock is S1 , S1 , S2 there would be a vacuous pass due to 2nd |=>

[Ben_A] You are referring to:
( ps == S1 ) |=> ( ps != S1 )[->1] ##0( ps == S3 ) |=> not( ( ps != S3 )[->1] ##0 (ps == S6) );

if (ps==S1) is false, the property is vacuous.
It would also be vacuous if under the dame condition you wrote:
( ps == S1 ) ##1 ( ps != S1 )[->1] ##0( ps == S3 ) |=> …

Thus, the first “|=>” does nothing for you, just makes it harder to read.
The antecedent is a precondition to test the consequent. Mutiple ones makes it more complex IMHO
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

Kushal_Nijalingappa · February 13, 2024, 6:28pm

I tried with a different approach.

(current_state == STATE_1)[*1:$] ##1 (current_state == STATE_2)[*1:$] |=> (current_state != STATE_3)[*1:$]).

Can this still cover all possible scenarios?

ben2 · February 13, 2024, 7:20pm

(current_state == S1)[*1:$] ##1 (current_state == S2)[*1:$] |=> (current_state != S3)[*1:$]).
/*From a requirement point of view, this says if S1 is eventually true and if S1 is immediately followed with S2, then this is followed by !S3 forever. Example: */
S1 S1 S1 S2 !S3  // pass 
S1 S1 S2 S3 // FAIL
// Can rewrite your code as 
(current_state == S1) ##1 (current_state == S2) |=> (current_state != S3)).
// (current_state == S1)[*1:$] ##1 (current_state == S2)[*1:$]
// the sequence S1[*2] ##1 S2 makes the antecedent vacuous
//  For nonvacuity you only need S1 followed by S2

Kushal_Nijalingappa · February 13, 2024, 8:27pm

Hello Ben,

I understood. But can you let me know why the below would logically fail? (although constant checking of current_state == S1 is not required)

(current_state == STATE_1)[*1:$] ##1 (current_state == STATE_2) => (current_state != STATE_3))

Also, I was not able to understand the below lines:
// the sequence S1[*2] ##1 S2 makes the antecedent vacuous
// For nonvacuity you only need S1 followed by S2

ben2 · February 13, 2024, 9:14pm

 //understood. But can you let me know why the below would logically fail? 
 //(although constant checking of current_state == S1 is not required)

(current_state == STATE_1)[*1:$] ##1 (current_state == STATE_2) => (current_state != STATE_3))
//Consider the threads: 
S1[*1] ##1 S2  // S1 S2 thread makes the assertion nonvacuous 
// If you have the sequence S1 S2 
//   then the other threads S1[*2], S1[*3], S1[*n] are all not a match 
//   (S1 S2 says that you do not have S1[*2] and all the others. 

// S1[*4] ##1 S2 => !S3 // S1 S1 S1 S1 S2 S3 is a fail, expecting !S3
// Again, you do not need the [*1:$] because the nonvacuous antecedent is the last S1 with S2

// [You] Also, I was not able to understand the below lines:
// the sequence S1[*2] ##1 S2 makes the antecedent vacuous
// For nonvacuity you only need S1 followed by S2
// [Ben] I did not convey the correct message, my apologies.
S1[*2] ##1 S2 is same as 
S1 S1 S2// thus if the input is S1 S2 the antecedent is vacuous. 
// If the sequence is 
S1 S1 S2 // then you have nonvacuity

Kushal_Nijalingappa · February 13, 2024, 9:41pm

I understood now. Thank you for the detailed explanation.

ben2 · February 15, 2024, 2:03am

More thoughts:

Q: How to simplify this property
	 (state== S1)[*1:$] ##1 (state== S2)[*1:$]  => (state= S3)[*1:$] 

  A: (state== S1) ##1 (state== S2)[*1:$] |=> (state= S3))
  Explanation: The antecedent has these threads: 
     (state== S1)[*1] ##1 (state== S2)[*1] or 
	 (state== S1)[*2] ##1 (state== S2)[*1] or 
	 ... 
     (state== S1)[*n] ##1 (state== S2)[*n];
    
	For the property to succeed, we need an attempt with state== S1 
	followed by state== S2 repeated n times until state== S3.
	Thus, with 	let T1=state==S1;  let T2=state==S2; let T3=state==S3;
	the following state value will make the property true:
	attempt number 
	1  2  3  4  5  6  7
	T1 T1 T1 T2 T2 T2 T3  // with the sequence attempted at attempt 3 being considered.     // Attempts 1, 2, 4, 5, 6, 7 make the property vacuous

ben2 · February 15, 2024, 4:10pm

UPDATED
SVA: Q: How to simplify this property
(state== S1)[*1:] ##1 (state== S2)[*1:] => (state= S3)[*1:$]

A: (state== S1) |-> ##1 (state== S2)[*1:$] ##1 (state= S3))
Explanation: For the property to succeed, we need an attempt with state== S1
followed by state== S2 repeated n times until state== S3.

For an assertion to be successful, two requirements must be met:

There must be no failure in the search of a matched antecedent with a consequent.
All threads of the antecedent and consequent must be successful. There are two types of successes: vacuous and nonvacuous.

ben2 · February 16, 2024, 11:34pm

SVA: Emulating “until” with a sequence:

This question came up from a user and my original response in https://lnkd.in/gxmA5gkm
/* Requirements: 
 If st==S1 and if it is then immediately followed by st==S2 for 1 or more cycles then S3 will follow the last S2. */
 // ILLEGAL Solution
 ap_illegal: assert property(@(posedge clk)
 $rose(st== S1) ##1 ((st== S2) until !(st==S2)) |-> (st==S3)); 
 // Illegal because the until is a property operator, needs a sequence for an antecedent 

 // Emulating the "until" with a sequence 
 ap_legal: assert property(@(posedge clk)
 $rose(st== S1) ##1 ((st== S2)[*1:$] ##1 1 intersect (st!=S2)[->1]) |-> (st==S3)) p2++; else f2++;
Notice the sequence that has a ##1 after the repeat and the 
 ((st== S2)[*1:$] ##1 1 intersect (st!=S2)[->1]) 
The intersect constraints the sequence to one choice. 
If that sequence matches, then we are in the cycle following the last S2, and thus we need the |-> operator.

Test code