In reply to ben@SystemVerilog.us:
Thanks Ben.
(1) I was trying to use same logic (with different equivalent expression) for ‘intersect’ operator .
The consequent begins evaluation at time:35. 1st grant is true at time:85 and 2nd grant is true at time:125
$rose(gnt)[=1] is equivalent to !$rose(gnt)[*0:$] ##1 $rose(gnt) ##1 !$rose(gnt)[*0:$] ,
// Since !$rose(gnt) is true from t:35 to t:75, i.e !$rose(gnt)[*5] is true in our case
// One of the possible LHS sequence is :
( !$rose(gnt)[*5] ##1 $rose(gnt) ##1 !$rose(gnt)[*0:$] )
// Which can be further expanded to
( !$rose(gnt)[*5] ##1 $rose(gnt) ##1 !$rose(gnt)[*0] ) or // 1st seq
( !$rose(gnt)[*5] ##1 $rose(gnt) ##1 !$rose(gnt)[*1] ) or
..................................................
( !$rose(gnt)[*5] ##1 $rose(gnt) ##1 !$rose(gnt)[*N] )
// 1st seq has an empty sequence !$rose(gnt)[*0] , hence it can be re-written as
( !$rose(gnt)[*5] ##1 $rose(gnt) ##0 `true ) // 1st seq
So why does assertion fail when 2nd grant is received ? Shouldn’t the single $rose(gnt) be sufficient for the LHS sequence to be a match ?
(2) In your equivalent expression I believe you have missed out on ##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:$] ##1 !$rose(gnt)[*0:$] // ##1 added
##1 $rose(gnt) ##1 !$rose(gnt)[*0:$] ##1 1[*0:$]) intersect $rose(req)[->1]