In reply to raku:
From my SVA Handbook
The first_match operator matches only the first of possibly multiple matches for an evaluation attempt of its operand sequence. This allows all subsequent matches to be discarded from consideration. This is significant when a sequence is used in the antecedent of an assertion because when a range is used in the antecedent, it can create multiple threads, each triggering the evaluation of the consequent when matched, and all threads must hold for the assertion to hold. This can cause significant performance impacts and possible unexpected errors. However, when a sequence is a subsequence of a larger sequence, then applying the first_match operator has significant (positive) effect on the evaluation of the enclosing sequence. Consider the following example:
ap_never_succeed: assert property(($rose(a) ##[2:$] b) |=> c);
The assertion ap_never_succeed is equivalent to
ap_equivalent_to_ap_never_succeed: assert property(($rose(a) ##2 b)or ($rose(a) ##3 b)or
… ($rose(a) ##n b)|=> c); // where n is infinity
For the ap_equivalent_to_ap_never_succeed assertion to succeed, all threads must succeed, and there are an infinite number of threads; specifically, these threads include:
($rose(a) ##2 b) |=> c // thread 1
($rose(a) ##3 b) |=> c // thread 2
…
($rose(a) ##n b)|=> c // thread n
If any of these threads fails, then the assertion fails; however success cannot be achieved. With the first_match method, only the first match of the sequence is considered, and all other threads are ignored. Thus, in the assertion ap_FM_can_succeed a first match of the antecedent is considered for the evaluation of the consequent.
ap_FM_can_succeed: assert property(
first_match($rose(a) ##[2:$] b) |=> c);
i am thinking use of first_match is if @cycle 2 thread 2 starts @cycle 5 antecedent of thread gets success so thread2 immediately check for stable valueof other signal . But still thread2 is not killed at @cycle7 again it antecedent gets success and again matches stable value of other signal .
Let me rephrase this with proper terms
i am thinking use of first_match is if
@cycle 2, thread@t2 (that is the name I gave to that independent, separate thread) starts.
@cycle 5 antecedent of thread gets success so thread@t2 immediately check for stable valueof other signal (the consequent). Since the consequent succeeds for thread@t2, that thread get kills, and is marked as a PASS. Now, we're DONE with that thread@t2.
@cycle 5, thread@t5 starts (this is the 1st occurrence of $fell(a).
@cycle7 again it antecedent for thread@t5 gets success and again matches stable value of other signal, Thus, at cycle 7, we're done with thread@t5 at that cycle 7; that thread@t5 is considered a PASS.
Another wasy of thinking about this is you standing on a corner of a one-way street.
A car with license plate 0001 passes by at t2.
At t5, car with license plate 0001 reaches its destination (the freeway); we're done with that car.
At t5, another car, with license plate 0002 passes the oorner where you stand.
At t7, car with license plate 0002 reaches its destination (the freeway); we're done with that car.
Every car is independent from other cars, and each car has its own destiny.
The first_match is to avoid multiple matches on a sequence, since all matches of an antecedent must comple before an assertion with implication completes. Example:
a ##[1:$]b |-> c // is same as
(a ##1 b) or (a ##2 b) or ... (a ##n b) |-> c
thius assertion can only fail, but cannot pass
first_match(a ##[1:$]b) |-> c // can pass because you do not test all possible combinations of this ORing, all you need is the first one that matches.
Ben SystemVerilog.us