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

From: Doron Bustan <dbustan_at_.....>
Date: Mon Oct 31 2005 - 14:49:13 PST
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 Mon Oct 31 14:49:28 2005

This archive was generated by hypermail 2.1.8 : Mon Oct 31 2005 - 14:50:41 PST