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

A different example to think about might be:

 

sequence  example;

@(posedge clk) $rose(a) ##2 proc1[*1:2] ##2 proc2;

endsequence

 

Say "a" rises at clk 4 and clk 6 such that there are two evaluations of the
endpoint in progress.  Now let's say that the evaluation that started at clk
4 is a match (1'b1) but the one that started at clk 6 is not a match (1'b0)
since it is still in progress.   What result is returned by
example.triggered?  I would think it would be an "or" of all the active
threads.  

 

Evaluation of an endpoint can result in multiple threads where first_match
does not help.  

 

Lisa

 

  _____  

From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] 
Sent: Sunday, October 25, 2009 9:53 AM
To: Bustan, Doron; 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 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  <http://www.mailscanner.info/> MailScanner, 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  <http://www.mailscanner.info/> MailScanner, and is 
believed to be clean. 


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