Difference in output using 'within' V/S 'intersect' operator

SystemVerilog
,
2

In reply to MICRO_91:
within V/S intersect operator(1) - EDA Playground // code
EPWave Waveform Viewer // wave


 ap1:assert property( @(posedge clk)$rose(req) |=>  
                     $rose(gnt)[=1] intersect $rose(req)[->1]) 
                      pass1=pass1+1; else fail1=fail1+1; 
                                    
 ap2:assert property( @(posedge clk)  $rose(req) |=>  
                      $rose(gnt)[=1] within $rose(req)[->1])
                        pass2=pass2+1; else fail2=fail2+1; 
1)  (seq1 within seq2) is equivalent to: ((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )
2)  $rose(gnt)[=1] is equivalent to !$rose(gnt)[*0:$] ##1 $rose(gnt) ##1 !$rose(gnt)[*0:$] ,
// expanding $rose(gnt)[=1] within $rose(req)[->1])
 (1[*0:$] 
   !$rose(gnt)[*0:$] ##1 $rose(gnt) ##1 !$rose(gnt)[*0:$] 
   ##1 1[*0:$])
   intersect $rose(req)[->1]
 // Consider the LHS of the intersect, this gets simplified to 
   (1[*0:$] !$rose(gnt)[*0:$] ##1 $rose(gnt) ##1 !$rose(gnt)[*0]] ##1 1[*0:$]) or // 1st
   (1[*0:$] !$rose(gnt)[*0:$] ##1 $rose(gnt) ##1 !$rose(gnt)[*1]] ##1 1[*0:$]) or  //2nd
   ..
   (1[*0:$] !$rose(gnt)[*0:$] ##1 $rose(gnt) ##1 !$rose(gnt)[*n]] ##1 1[*0:$]) or  //nth
  // We don't need the 2nd, ...nth. because the 1st of the ORed sequences is sufficient here  
  // consider the 1st 
   (1[*0:$] !$rose(gnt)[*0:$] ##1 $rose(gnt) ##1 !$rose(gnt)[*0]] ##1 1[*0:$])
   // get reduced to the following because of the [*0].  (a[*0] ##1 b) is reduced to (b)
   (1[*0:$] !$rose(gnt)[*0:$] ##1 $rose(gnt) ##1 1[*0:$])
   // THUS, the assertion does not test fora 2nd occurrence of $rose(gnt). 
   // a 2nd occurrence of $rose(gnt) does not cause a fail
   // For a pass, all we need here with the within is a single occurrence of $rose(gnt).

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

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog