In reply to MICRO_91:
I am looking at this
within V/S intersect operator(1) - EDA Playground // code
EPWave Waveform Viewer // wave
For an intersect operator to pass,LHS sequence must be of the same length as the RHS sequence
Example
a[=1] intersect b[->1]) // equivalent to, as you stated
!a[*0:$] ##1 a ##1!a[*0:$] intersect !b[*0:$] ##1 b //
// assume that the length of the sequence b[->1] is 5 cycles.(b==1 after 4 cycles from start)
// the threads of the LHS that can only be in consideration are
a[*1] ##1 !a[*4]
!a[*1] ##1 a ##1 !a[*3]
!a[*2] ##1 a ##1 !a[*2]
!a[*3] ##1 a ##1 !a[*1]
!a[*4] ##1 a
// If the LHS is as follows
!a ##1 a ##1 !a ##1 a ##1 !a // we have 2 occurrence of a
// An optimized simulator would recognized that there is no need to further evaluate
// the LHS since anything thread after (!a ##1 a ##1 !a ##1 a) is a no-match even if it
// length-match the RHS. This is because the LHS is a[=1].
// Thus, at the end of the thread of length 4 the simulator can declare a failure.
within V/S intersect operator(2) - EDA Playground code
EPWave Waveform Viewer wave
// With code as shown in above link, replacing the intersect with "and"
// causes a pass because the "and" does not require length-matching
ap1:assert property( @(posedge clk)$rose(req) |=>
$rose(gnt)[=1] and $rose(req)[->1])
// $rose(gnt)[=1] intersect $rose(req)[->1])
pass1=pass1+1; else fail1=fail1+1;
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