SVA Assertions using only $realtime and nested implications

SystemVerilog
, , ,
1

My current requirement is to check the behavior of 2 signals. ‘state_var’[3:0] and then ‘status’ 1 bit. (this goes high for just 1 clk cycle)

I need to check / verify behavior of ‘status’ signal which has to become in the interval of Min- 2us & Max 8us after ‘state_var’ transitions from 'h00-> ''h02
Here state_var is on (negedge of clk) and ‘status’ is on posedge of clk, So, should i use posedge or negedge both in sensitivity list?

I tried different things like
1.)

real time_stamp;
@(negedge clk) (state_var == 2 && $past(state_var, 1) == 0)  ##0 (1, timestamp = $realtime) |-> ##[0:$] $rose(status) |-> (($realtime - timestamp > 2us) && ($realtime - timestamp < 8us));

2.)

real time_stamp;
@(negedge clk) (state_var == 2 && $past(state_var, 1) == 0)  ##0 (1, timestamp = $realtime) |-> first_match(##[0:$] $rose(status)) |-> (($realtime - timestamp > 2us) && ($realtime - timestamp < 8us));

This throws Error saying- Property operator usage is not allowed in sequence context. Implication used with first_match, first_match can be applied only to a sequence.).

3.)

real time_stamp;
@(negedge clk) (state_var == 2 && $past(state_var, 1) == 0)  ##0 (1, timestamp = $realtime) |-> ##[0:$] $rose(status) ##0 (($realtime - timestamp > 2us) && ($realtime - timestamp < 8us));

But nothing is working so I want some insights, This is my first time working with such SVA assertions. I believe 3rd one is the correct one, but need some insights.

2
  1. Never use the form:
    seq1 |-> seq2 | seq3;
    It has too many implication operators.
    Consider using vounts instead of time, unless there are good reasons for it, like lack of clocking events. Time does not work well in formal verification.
property p_state_status;
  realtime time_stamp;
  @(negedge clk) $rose(state_var == 2 && $past(state_var, 1) == 0) 
       ##0 (1, timestamp = $realtime) |-> @(posedge clk) $rose(status)[->1] 
       ##0 (($realtime - timestamp > 2us) && ($realtime - timestamp < 8us));
endproperty 


// Assume that 2us is a posedge count of 100
property p_state_status2;
  int v;
  @(negedge clk) ($rose(state_var == 2 && $past(state_var, 1) == 0), v=0) |->
        @(posedge clk) (1, v=v+1)[*0:$] ##1 $rose(status)  ##0  
        V>=100 && v<=400;
endproperty
1 Like
3

More thoughts on style:

/* Separate the "cause" from the "effect"
  In this case, the "cause" (antecedent) is the sequence from state_var until the new status. 
  The "effect" (consequent} is the verification (or test) of the duration 
*/
// DO THIS INSTEAD
property p_state_status;
  realtime time_stamp;
  @(negedge clk) $rose(state_var == 2 && $past(state_var, 1) == 0) 
       ##0 (1, timestamp = $realtime) ##0 @(posedge clk) $rose(status)[->1]  |->
          ##0 (($realtime - timestamp > 2us) && ($realtime - timestamp < 8us));
endproperty
1 Like
4

Can you comment on Solution 3 I gave? It’s working as well. So, Want your opinion

5

Your solution 3 works pretty much like my solution in my last post.
What I did not like in your solution is the style.
From a readability standpoint, I prefer to have in the antecedent all the causes (or sequences) that create the things to verify (I. E., consequent).
Thus, the antecedent are typically inputs, and the consequent the expected outcome.

1 Like