Assertion to check variable distance of two signals

SystemVerilog
, , ,
1

I’d like to write an assertion to check the distance between two signals like the following.

//              len > 0
//             _________
// s1    :  __|<-------> __
// s2    :     _________|
//             + + + + +
// v_cnt :     1 2 . .len len
//             ^...........*
property p_inter_pos_length(s1, s2, len);
  int v_cnt = 0;
  $rose(s1) ##0 first_match( (s1 && !s2, v_cnt++)[*1:$] ##1 s2 ) |-> (v_cnt == len);
endproperty

However, this doesn’t work with len==0. The situation of $rose(s1) ##0 $rose(s2) with len==0 is also valid. So, I’d like to include len==0 case to the property. Variable wait sequence in stead of variable s1 continuation like the following might be considered.

$rose(s1) ##0 first_match( (1,v_cnt++)[*0:$] ##0 s2) )

But no s2 rising edge after s1 rising edge is possible.

         ____________       __________
s1  : __|            |_____|
                                        __
s2  : _________________________________|

So, I don’t think the idea of variable wait above is applicable.

Does anyone have any good property ideas to resolve this matter in this situation?

2

Try ::

// Consequent has implicit first_match
property p_inter_pos_length;
 realtime t1,t2;
 ($rose(s1),t1=$realtime) |-> ($fell(s1)[->1]) or (($rose(s2)[->1],t2=$realtime) ##0 ( (t2-t1) > 0 ));
endproperty
ap1:assert property( @(posedge clk) p_inter_pos_length ) <pass> else <fail>

What is the intention in following case ::
After 1st assertion of s1 (0->1), s1 is de-asserted (1->0) at the same time as s2 is asserted (0->1) ?
Using the above code the assertion would pass due to ‘or’ at de-assertion of s1

3

Thank you for your proposal. But it looks the property you proposed is different from what I want to check. What I want to check is
“whether the clock cycle number between rising edges of two signals is same as the specified value.”

No, s1 is kept high when s2 is asserted(0->1). But this s1 behavior is not quite related to this matter. The point is how to count cycle number before s2 assert(0->1).

4

I hit upon the following property idea.

//               len >=0
//              ______________
// s1    :   __|<---------> __      
// s2    :      ___________|
//              + + + + + + +
// v_cnt :   -1 0 1 2 3 . .len len
//            ^.................*
property p_inter_pos_length(s1, s2, len);
//int v_cnt = 0;
//        $rose(s1) ##0 first_match( (s1 && !s2, v_cnt++)[*1:$] ##1 s2 ) |-> (v_cnt == len);
  int v_cnt = -1;
  !s1 ##1 $rose(s1) ##0 first_match( (s1       , v_cnt++)[*1:$] ##0 s2 ) |=> (v_cnt == len);
endproperty

I think this would work.

5

If you insist on using a counter approach I would suggest a few changes to your code

  1. Using !s1 ##1 $rose(s1) , is it necessary for s1 to be low in the start ?
    What if you simply used $rose(s1) instead ?
  1. Any particular reason you have used non-overlapping implication operator |=> ?
    When the antecedent has a match, you could check the consequent at the same clock using |->

Here is my attempt using counter logic :: edalink

1 Like
6

Thank you for your suggestion.

The reason why I used 1. !s1 ##1 $rose(s1) and 2 . |=> is similar. I just wanted
to separate internal counter increment cycle from counter initialization cycle and check cycle. By 1, I wanted to clarify counter initialization and counter increment are done in a different cycle. By 2, the check is done after the last counter increment cycle. They are only for safety just in case. A property without them would properly work as you have attempted in EDA Playground.

property p_inter_pos_length(s1, s2, len);
//int v_cnt = 0;
//        $rose(s1) ##0 first_match( (s1 && !s2, v_cnt++)[*1:$] ##1 s2 ) |-> (v_cnt == len);
  int v_cnt = -1;
//!s1 ##1 $rose(s1) ##0 first_match( (s1       , v_cnt++)[*1:$] ##0 s2 ) |=> (v_cnt == len);
          $rose(s1) ##0 first_match( (s1       , v_cnt++)[*1:$] ##0 s2 ) |-> (v_cnt == len);

endproperty

In that case, the internal counter would work like below.

//              ______________
// s1    :   __|<---------> __      
// s2    :      ___________|
// v_cnt :     -1
//              + + + + + + +
//              0 1 2 3 . .len
//              ^...........*
7

Another idea.

If you don’t like to initialize v_cnt with -1, then, the following is fine.

//              ______________
// s1    :   __|<---------> __      
// s2    :      ___________|
// v_cnt :      0
//              + + + + + +
//              1 2 3 . .len len
//              ^............*
property p_inter_pos_length(s1, s2, len);
  int v_cnt = 0;
  $rose(s1) ##0 first_match( (s1, v_cnt += !s2)[*1:$] ##0 s2 ) |-> (v_cnt == len);
endproperty

v_cnt is incremented only when s2 is low while s1 is high. So, v_cnt is not incremented at the last cycle.

Here is a link to EDA Playground.
EDA Playground : SVA Dynamic Variable Signal Distance Check

8

There is a large number of experts who abhor the use of the first_match
because of efficiency; also, it is not used in PSL.
Below is another option without the first_match.
I like the v_cnt += !s2

//              ______________
// s1    :   __|<---------> __      
// s2    :      ___________|
// v_cnt :      0
//              + + + + + +
//              1 2 3 . .len len
//              ^............*
property p_inter_pos_length(s1, s2, len);
  int v_cnt = 0;
  // $rose(s1) ##0 first_match( (s1, v_cnt += !s2)[*1:$] ##0 s2 ) |-> (v_cnt == len);
  ($rose(s1) ##0 (s1, v_cnt += !s2)[*1:$]) intersect s2[->1] |-> (v_cnt == len);
endproperty

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

1 Like
9

Thanks, Ben,

I will replace first_match with intersect s2[->1].

But note that a certain license free simulator doesn’t properly work with intersect s2[->1] while first_match usage is O.K . It is simulator’s issue, though.

10

Hello. Can anyone let me know what this expression

(s1, v_cnt += !s2)

exactly does? I was able to understand that increment count till s2 becomes high. But why are we checking on s1?

11

Hi @Kushal_Nijalingappa ,

It means “v_cnt is incremented while s1 is 1 except s2 is 1”.

I wanted to check the distance between s1 rise and s2 rise. So, the condition of s1 == 1 is necessary. Otherwise, the following distance would also be checked with (1, v_cnt += !s2)

//         _____________      _______________
//s1  : __|^           |_____|             __
//s2  : __________________________________|*
//         ^...............................*
//         + + + + + + + + + + + + + + + +
2 Likes