In reply to MICRO_91:
ap1:assert property( @(posedge clk)$rose(req) |=>
$rose(gnt)[=1] intersect $rose(req)[->1])
pass1=pass1+1; else fail1=fail1+1;
//Assertion fails at t 122.5 when the 2bd gnt is seen.
// 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
// BUT for an intersect the thread of the
// LHS sequence must be of the same length as the tread of the RHS sequence
// Thus, for the "//1st seq" that would occur only if $rose(req)[->1] occurred in that cycle.
// It did not in that sim. Thus, you need to consider the other ORs
// 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 NO INTERSECT yet
( !$rose(gnt)[*5] ##1 $rose(gnt) ##1 !$rose(gnt)[*1] ) or
..................................................
( !$rose(gnt)[*5] ##1 $rose(gnt) ##1 !$rose(gnt)[*N] )
Ben