In reply to Adarsh24:
b[->1] is equivalent to: !b[*0:$] ##1 b
At every clocking event there is an attempt at the assertion, meaning that a new thread, independent from other threads, starts to evaluate the antecedent and consequent. Use the $rose unless you need to check the consequent for every clocking event when antecedent is true.
You’re correct, “(c && (reg2[16:0] == 17’hF))” is expr1; I misread it.
Or do u mean antecednt can have a sequence with multiple events and then if we need first of those events, use first_match?
when antecedent has “or”.
a ##[1:2] b is equivalent to
a ##1 b or a ##2 b.
C[*1:2] ##1 d is equivalent to
C [*1] ##1 d or C[*2] ##1 d
Read my paper - Understanding the SVA Engine,