The SYSTEM VERILOG ASSERTIONS HANDBOOK, 4th Edition states following on page no. 36:
Do not use first_match function in a sequence that is an antecedent that has goto repetition operator unless that sequence has other expressions which are multi-ranged.
Thus a ##1 b[->1] |-> c; //first_match is not needed here because once b==1, there could not be another thread of !b.
The book also states on page no. 37 that for non-consecutive repetition operator, in an antecedent, we NEED TO USE first_match function:
a ##1 b[=1]##1 c |-> d; is equivalent to
a ##1 !b[*0:] ##1 b ##1 !b[*0:] ##1 c |-> d;
// !b[*0:$] ##1 c can cause mutliple threads.
(can someone explain why this causes multiple threads?)
Now above statement is equivalent to !b[*0] ##1 c or !b[*1] ##1 c or !b[*2] ## 1 c … and so on. ( !b ## 1 c or !b ##1 !b ## 1 c …)
Are the multiple threads caused by or operator in the above expression?
In that case even for goto operator example given above - a ##1 b[->1] |-> c;
There will be multiple threads as b[->1] is equivalent to !b[*0:$] ##1 b; Why does this not cause multiple threads (because of repetition of !b)
The SYSTEM VERILOG ASSERTIONS HANDBOOK, 4th Edition states following on page no. 36:
Do not use first_match function in a sequence that is an antecedent that has goto repetition operator unless that sequence has other expressions which are multi-ranged.
Thus a ##1 b[->1] |-> c; //first_match is not needed here because once b==1, there could not be another thread of !b.
The book also states on page no. 37 that for non-consecutive repetition operator, in an antecedent, we NEED TO USE first_match function:
a ##1 b[=1]##1 c |-> d; is equivalent to
a ##1 !b[*0:] ##1 b ##1 !b[*0:] ##1 c |-> d;
// !b[*0:$] ##1 c can cause mutliple threads.
(can someone explain why this causes multiple threads?)
[Ben]
!b[*
a ##1 b[=1]##1 c |-> d; is equivalent to
a ##1 !b[*0:$] ##1 b ##1 !b[*0:$] ##1 c |-> d; // correct, expanded to:
(a ##1 !b[*0] ##1 b ##1 !b[*0] ##1 c) or
(a ##1 !b[*1] ##1 b ##1 !b[*0] ##1 c) or
(a ##1 !b[*n] ##1 b ##1 !b[*0] ##1 c) or
...
(a ##1 !b[*0] ##1 b ##1 !b[*1] ##1 c) or
(a ##1 !b[*0] ##1 b ##1 !b[*2] ##1 c) or
(a ##1 !b[*0] ##1 b ##1 !b[*n] ##1 c) or
..
(a ##1 !b[*1] ##1 b ##1 !b[*1] ##1 c) or
(a ##1 !b[*1] ##1 b ##1 !b[*2] ##1 c) or
(a ##1 !b[*1] ##1 b ##1 !b[*n] ##1 c) or
....
(a ##1 !b[*n] ##1 b ##1 !b[*1] ##1 c) or
(a ##1 !b[*n] ##1 b ##1 !b[*2] ##1 c) or
(a ##1 !b[*n] ##1 b ##1 !b[*n] ##1 c) |-> d
// There are lots of other possible matches after b==1
// and without a first_match() they all have to be tested
Are the multiple threads caused by or operator in the above expression?
Yes, as explained above
In that case even for goto operator example given above - a ##1 b[->1] |-> c;
There will be multiple threads as b[->1] is equivalent to !b[*0:$] ##1 b; Why does this not cause multiple threads (because of repetition of !b)
a ##1 b[->1] |-> c // equivalent to
a ##1 !b[*0] ##1 b |-> c; // equivalent to
a ##1 !b[*1] ##1 b or
a ##1 !b[*2] ##1 b or
,,
a ##1 !b[*n] ##1 b |-> c;
// If the tread (a ##1 !b[*1] ##1 b ) is a match with b==1 then
// All the other threads are false
// a ##1 !b[*1] ##1 b means a==1 ##1 b==0 ##1 b==1 // Then
// a ##1 !b[*2] ##1 b // is a no match because we saw the sequence b==0 ##1 b==1
// thus b==0 ##1 b==0 is a no match, and so are all of the other sequences.
// The simulator does not test all the other possibilities since once you find one match
// Alll of the others are not a match.
-sunil puranik[/quote]
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.