In reply to ben@SystemVerilog.us:
Ben , two follow up questions
(1) Assume antecedent is True at Clock tick T0 , and the ’ ack ’ is received at T5
So the assertion would Pass at T5 .
I have following understanding of the consequent . Please correct me if wrong .
LHS of intersect operator is :: *( !ack[0:] ##1 ack ##1 !ack[*0:] ) .
It’s equivalent to ::
( !ack[*0] ##1 ack ##1 !ack[*0:$] ) or ( !ack[*1] ##1 ack ##1 !ack[*0:$] ) or
( !ack[3] ##1 ack ##1 !ack[*0:$] ) or ( !ack[*4] ##1 ack ##1 !ack[*0:$] ) or ....
( !ack[*0:$] ) is equivalent to ( !ack[*0] or !ack[*1] or !ack[*2] or .... )
So one such sequence from the infinite possible sequence is
( !ack[*4] ##1 ack ##1 !ack[*0] ) // This sequence is True for T1 to T5 .
As consequent has an implicit "first_match" , if any 1 of the infinite
combination is True the LHS of ' intersect ' operator is True .
(2) Is the above solution an alternative to your unique solution in :: Uniq_Ack