RE: [sv-ac] Semantics of "calling subroutines on match of a seque nce" is not well defined.

From: Bassam Tabbara <Bassam_at_.....>
Date: Tue Nov 01 2005 - 09:06:57 PST
Hi Doron,

Just a quick comment on my initial feel for this, and focusing on the
last example in the discussion.

 sequence s3;
 logic [2:0] v;

 (
 ((a ##1 a), v=1)
 or
 ((b ##1 b), v=2)
 )                   <<<< join happens here ...
##1 (c, $display("c, v=%d", v));

 endsequence,

I think that they key question is where the join happens. In the case
above I think the LRM is clear that the join happens where I have the
mark. If you had wished to have visibility into "v" inside the 2 threads
then you would nee dot add a $display inside. I feel this is the right
interpretation/treatment that preserves visibility/consistent treatment
(e.g. I can swap the threads with named sequences and have similar
treatment). Again the $display (despite that it's "read only") should
have the same rights as anything in that portion of the sequence after
the join.

** Of course, the top-level directive can affect what data to
keep/report, but that's an orthogonal issue, for now assume we are
reporting all the threads (cover (sequence) say).

** As for *[..] and ##[..] constructs, the LRM does treat those as a
join at the TOP level so I think the interpretation that the $display
should commute on all the sub-threads is valid.

Thx.
-Bassam.

--
Dr. Bassam Tabbara
Architect, R&D
Novas Software Inc.
(408) 467-7893

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Doron Bustan
Sent: Monday, October 31, 2005 2:49 PM
To: vhdlcohen@aol.com
Cc: Bustan Doron-DBUSTAN; sv-ac@eda.org
Subject: Re: [sv-ac] Semantics of "calling subroutines on match of a
seque nce" is not well defined.

Ben,

First let's agree that the LRM does not answer my questions.  I  think
that threads semantic is not defined in the LRM, and thus, different
people may have different valid approaches. Do you agree?

I agree that we need a different approach for sequences in
cover/antecedent/consequent but I think the overall solution should be
consistent, and should not be tool dependent.

In the first example I think that your interpretation for the sequence
sequence s1;  ((a[*1:3] , $display("aa")) #1 b)  and  c[*6];
endsequence  is correct, and I don't see ambiguity for it.

In the second example, I think you gave a bad example.
The LRM defines the local variable that  flow out of an or of two
sequences  (s1 or s2), as the intersection of the local variables that
flows out of s1, and the local variables that flows out of v2. Thus, the

 sequence s3_modified;
 logic [2:0] va, vb;
 (
 ((a ##1 a), va=1)
 or
 ((b ##1 b), vb=2)
 ) ##1 (c, $display("c, va=%d, vb=%d", va, vb));  endsequence

is not legal, because va and vb do not flow out of

 (
 ((a ##1 a), va=1)
 or
 ((b ##1 b), vb=2)
 )

I think that for the sequence

 sequence s3;
 logic [2:0] v;

 (
 ((a ##1 a), v=1)
 or
 ((b ##1 b), v=2)
 ) ##1 (c, $display("c, v=%d", v));

 endsequence,

it is clear that in an antecedent or in a cover property there should be
two displays, one for each "thread". I think that this  should also be
the case, when the sequence is in a consequent, but I agree that
currently it is a wild interpretation of the LRM.

Doron


vhdlcohen@aol.com wrote:

> Doron,
>   I Believe that in general the answer lies as to whether that 
> sequence is an antecedent, a consequent, or is used in a cover 
> directive. This statement is because of possible multiple matches.
>  sequence s1;
>  ((a[*2] , $display("aa")) #1 a)
>  intersect
>  b[*3];
>  endsequence
>   If "b" is low in the first cycle of computation for thread x, then 
> the sequence fails.
>   An an antecedent the property is vacuously true, and the simulator 
> need not continue any evaluation for thread x.
>   As a consequent, the property fails and the simulator need not 
> continue any evaluation for thread x.
>   As a cover, the sequence fails and coverage for that thread is also 
> falso.
>   Thus, in that case, I consider it proper that the $display would 
> never trigger, thus your approach 2 is correct.
>
>  Now consider this example:
>  sequence s1;
>  ((a[*1:3] , $display("aa")) #1 b)
>  and
>  c[*6];
>  endsequence
>  Assume a==1 and b==1 and c==1 for all cycles:
>  As an antecedent, you have multiple matches  a and a display  aa and 
> a display  aaa and a display
>
>  As a consequent, you'll have one display since the property succeeds.
>
>  << I can see two different approaches
>   1. Consider only the subsequence (a[*2] , $display("aa")). Since 
> this subsequence
>   matches the prefix of the computation, the $display should be 
> executed after the second cycle.
>
>   2. Consider the whole sequence. Since in the first cycle of the 
> computation b is low,
>   the sequence fails at cycle 1, and thus, the $display should not be 
> executed. >>
>
>  ----
>   On the cases shown below, the $display will be executed ONCE. For 
> your sequence 3,
>   The displayed value of v is not determined, and could be = 1, or to 
> 2, depending upon the  simulator's order of evaluation. There is NO 
> guarantee.
>   There are many things that can cause unexpected results. In your 
> sequence s3, the user needs to be careful in the naming of the local 
> variable. Thus,  sequence s3_modified;  logic [2:0] va, vb;  (  ((a 
> ##1 a), va=1)  or  ((b ##1 b), vb=2)
>  ) ##1 (c, $display("c, va=%d, vb=%d", va, vb));  endsequence
>
>  << At the sequence
>  sequence s2;
>  ( (a #1 a) or (b #1 b) ) #1 (c, $display("c"));  endsequence
>
>   The question is not whether the $display should be executed after 
> cycle 3, but how many times:
>   once or twice. To make this more clear, consider the following 
> sequence
>
>  sequence s3;
>  logic [2:0] v;
>
>  (
>  ((a ##1 a), v=1)
>  or
>  ((b ##1 b), v=2)
>  ) ##1 (c, $display("c, v=%d", v));
>
>  endsequence
>
>  For a computation where a,b, and c are high in the first
>  3 cycles, I would expect 2 executions of the $display, one with  v = 
> 1, and the other with v=2.
>
>   So in the case of s2 haw many times the $display should be execute 1

> or 2? >>
>
>
>  Doron
>
>  vhdlcohen@aol.com wrote:
>
>  > Doron,
>  > My understanding is below:
>  > sequence s1; ((a[*2] , $display("aa")) #1 a) intersect b[*3];  > 
> endsequence  > At the the second "a", the endpoint of the sequence 
> a[*2] and  > regardless of combinations of "aa",  > the $display 
> should be executed.
>  >
>   > "In other cases it is not clear how many times a subroutine should

> be  > called  > in a given cycle. For example in the sequence  > 
> sequence s2; ( (a #1 a) or (b #1 b) ) #1  > (c, $display("c"));  > 
> endsequence  > In case that a,b, and c are high at the first 3 cycles,

> it is not  > clear how many times the $display should be executed. "
>  >
>  > Same thing here, at then endpoint of "( (a #1 a) or (b #1 b) ) #1 
> ",  > when "c" is reached ,  > and regardless of the value of "a" or 
> "b", the $display should be  > executed.
>   > In the above example, a user would want to put such subroutines in

> the  > consequent rather than the antecedent.
>  >
>  > Any disagreement to my opinions?
>  >
>   > >
> ----------------------------------------------------------------------
> ---
>
>  > -
>  > Ben Cohen Trainer, Consultant, Publisher (310) 721-4830  > 
> http://www.vhdlcohen.com/ ben_ f rom _abv-sva.org
>   > * Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN
> 0-9705394-7-9
>  > * Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 
> 2nd  > Edition, 2004, ISBN 0-9705394-6-0
>   > * Real Chip Design and Verification Using Verilog and VHDL, 2002 
> isbn  > 0-9705394-2-8  > * Component Design by Example ", 2001 isbn 
> 0-9705394-0-1  > * VHDL Coding Styles and Methodologies, 2nd Edition, 
> 1999 isbn  > 0-7923-8474-1  > * VHDL Answers to Frequently Asked 
> Questions, 2nd Edition, isbn  > 0-7923-8115
>   > >
> ----------------------------------------------------------------------
> ---
>
>  > --------
>  >
>  > >
>
>
>  
>
Received on Tue Nov 1 09:07:01 2005

This archive was generated by hypermail 2.1.8 : Tue Nov 01 2005 - 09:08:03 PST