[sv-ac] SVA: Clarification: Is result of .triggered a boolean or a sequence ?

LRM: *16.9.11 Detecting and using end point of a sequence ...The end point
of a sequence is reached whenever the ending clock tick of a match of the
sequence is reached, regardless of the starting clock tick of the match. The
reaching of the end point can be tested by using the method triggered.
 .... When method triggered is evaluated in an expression, it tests whether
its operand sequence has reached its end point at that particular point in
time. The result of triggered does not depend upon the starting point of the
match of its operand sequence.*

[Ben] Thus, the .*triggered *produces just a boolean that identifies the end
point of a sequence, regardless of when it started.  I read this as also
stating that if a sequence has a range, it may have multiple threads, and
each matching thread generates an individual end point.  Since the result of
a *.triggered* is a boolean, and not as a sequence, I claim that the result
of *first_match*(sequence_instance.*triggered*) is same
as sequence_instance.*triggered.  *
Here is the situation:
* sequence *q_b*;   @ (posedge clk) $rose(*a) *##*[1:*$*] b;*   endsequence
*: q_b
P1:  *assert property* (
     @ (*posedge *clk) * first_match(*q_b.*triggered*) |=> c);
Assume that "a==1"  for ONLY ONE cycle, and false forever thereafter (i.e.,
a has a single $rose. )
Assume that "b==1" for  all cycles. // thus q_b has a successful attempt,
and has multiple threads.
Assume that "c==0" for all cycles. // property  fails for any of the
threads.

In this model, sequence q_b has multiple threads for the 1st successful
attempt.  I claim that the antecedent*
**first_match(**q_b.**triggered**)*has multiple threads, and not one
thread
*. * Thus, the *first_match* does nothing because each end point of
q_b.*triggered
*is a boolean expression, and *first_match* of a boolean is same as
boolean.
I tested this on one simulator, and it behaved that way.
Ben cohen

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.