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

Hi Doron,

I think that Ben is right, you cannot distinguish multiple setting of the conceptual (and real) boolean by several threads/attempts.

ed


From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Bustan, Doron
Sent: Sunday, October 25, 2009 4:02 AM
To: ben@systemverilog.us; sv-ac@server.eda.org; Lisa Piper; Seligman, Erik; Korchemny, Dmitry
Subject: RE: [sv-ac] SVA: Clarification: Is result of .triggered a boolean or a sequence ?

Hi Ben,

I disagree. In your example every attempt has one thread (not sure thread is defined in the LRM), and all attempts fail.
So, the multiple match of q_b, just means that there are multiple attempts where the triggering Boolean is true.



Doron
________________________________
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of ben cohen
Sent: Sunday, October 25, 2009 4:21 AM
To: sv-ac@server.eda.org; Lisa Piper; Seligman, Erik; Korchemny, Dmitry
Subject: [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<http://www.mailscanner.info/>, and is
believed to be clean.

---------------------------------------------------------------------

Intel Israel (74) Limited



This e-mail and any attachments may contain confidential material for

the sole use of the intended recipient(s). Any review or distribution

by others is strictly prohibited. If you are not the intended

recipient, please contact the sender and delete all copies.

--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.

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