How the within syntax is working in SVA

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