How the within syntax is working in SVA

SystemVerilog
, ,
1

Hi There,

I am trying to check the occurrence of seq1 within seq2 so i tried the following formula:

property xyz;
@(posedge clk);
(fell(a) ##[1:] $rose(b)) within (rose(a) ##[1:] $rose(c));
endproperty

i am expecting that only if the signal ‘a’ has fell edge, the rose edge of signal ‘b’ should happen within the window of rose edge ‘a’ to rose edge ‘c’… but actually what happening is, the assertion is failing in each clock cycle where signal ‘a’ doesn’t have a fell edge… can any one please tell me why?

2

In reply to noha shaarawy:

Your property is checking at every clock edge that ‘a’ fells probably you want this

property xyz;
@(posedge clk)
$fell(a) |-> ##[1:$] $rose(b) within ($rose(a) ##[1:$] $rose(c));
endproperty

I need to simulate an example but it think this means when a fells b should go high at some point within the sequence a followed by c.

HTH,
-R

3

In reply to noha shaarawy:


    // i am expecting that only if the signal 'a' has fell edge, 
    //the rose edge of signal 'b' should happen within 
    //the window of rose edge 'a' to rose edge 'c'.. but actually 
    //what happening is, the assertion is failing in each clock cycle 
    //where signal 'a' doesn't have a fell edge.. 
    property BAD_xyz;
        @(posedge clk);
        ($fell(a) ##[1:$] $rose(b)) within ($rose(a) ##[1:$] $rose(c));
    endproperty
    // property BAD_xyz will fail at every attempt (e.g., clocking event ) 
    // because you cannot have a $fell(a) and $rose(a) in the same cycle.
    // You meant 
    property Better_but_still_BAD_xyz; // No antecedent
        @(posedge clk);
        ($fell(a) ##[1:$] $rose(b)) within 
           ($rose(a)[->1] ##[1:$] $rose(c));
    endproperty

    property xyz_OK;
        @(posedge clk);
        ($fell(a) |-> $rose(b)[->1] within 
                      $rose(a)[->1] ##1 $rose(c)[->1];
    endproperty
    // xyz_OK says: if($fell(a)) then 
    // a single occurrence of r should occur within 
    // a single occurrence of rose(a) follwoed by a 
    // a single occurrence of rose(c)

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

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
4

Hi Ben,

the following assertion is marked as an incomplete assertion in my simulation although on the waves itself, all the conditions are being met successfully… do you have any idea why it could happen?

property xyz_OK;
@(posedge clk);
$fell(a) |-> $rose(b)[->1] within $rose(a)[->1] ##1 $rose(c)[->1];
endproperty

5

In reply to noha shaarawy:
The sequence containment within specifies a sequence occurring within another sequence. Thus


$fell(a) |-> $rose(b)[->1] within $rose(a)[->1] ##1 $rose(c)[->1];

States that following a fell(a), there is an occurrence of a rose(b) followed by whatever (unspecified); that sequence is represented with the $rose(b)[->1].
That occurrence of rose(a) is within an occurrence of rose(a) followed by a rose(c).
Nothing specifies here what happens after the first occurrence of rose(a). Thus, the following sequence satisfies this assertion: \

t 1 2 3 4 5 6 7 8 9 A B C D E F
a 1 1 1 0 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
b 0 0 0 0 0 0 0 1 0 0 1 0 0 0 1 0 0 0 
c 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 
fell(a) at t4
rose(b) at t8 and tB and tF
rose(a) at t6 and at tA
rose(c) at tE 
$fell(a)at t4 |-> 
$rose(b)at t8 within 
  $rose(a)t6  followed by $rose(c) at tE; // PASS

Compare this to


ap_intersect: assert property( // I HAVE ISSUES WITH THE NEED of the first_match() HERE
//            AM DISCUSING THIS WITH THE VENDOR 
       @(posedge clk)
       $fell(a) |-> $rose(b)[=1] intersect $rose(a)[=1] ##1 $rose(c)[->1]); 
    
    ap_fmintersect: assert property(  // THIS WORKS, WHAT IS NEEDED                   
      @(posedge clk)
      $fell(a) |-> $rose(b)[=1] intersect first_match($rose(a)[=1] ##1 $rose(c)[->1]));

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

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
6

In reply to ben@SystemVerilog.us:

Hi Ben,
What is the problem without antecedent?
It seems this property can work.
Thank you

property Better_but_still_BAD_xyz; // No antecedent
    @(posedge clk);
    ($fell(a) ##[1:$] $rose(b)) within 
       ($rose(a)[->1] ##[1:$] $rose(c));
endproperty
7

In reply to peter:

property Better_but_still_BAD_xyz; // No antecedent
@(posedge clk);
(fell(a) ##[1:] $rose(b)) within
(rose(a)[->1] ##[1:] $rose(c));
endproperty
At every attempt, you start a new thread regardless of the value of $rose(a).
If the sequence (rose(a)[->1] ##[1:] $rose(c)) lasts 100 cycles, as an example,
then you have 99 unnecessary threads.
An antecedent prevents an overloading of redundant threads.
Take a look at your requirements and add an antecedent, my recommnedations.
Ben,

8

Ben,
A more fundamental question. In this:
$fell(a) |-> $rose(b)[->1] within $rose(a)[->1] ##1 $rose(c)[->1];

$rose(a)[->1] ##1 $rose(c)[->1] - means c should rise one clk cycle AFTER a rises, isn’t? If the spec calls for : c should arrive ANY clk cycle after a rises, should’nt the syntax be:
$rose(a)[->1] ## [*1:$] $rose(c)[->1]. Can you pls help? I am still new to SVA.

Many thanks.