Subject: Re: [sv-ac] revised local variable proposal
From: John Havlicek (john.havlicek@motorola.com)
Date: Mon Mar 17 2003 - 08:13:04 PST
Hi Jay:
For instances of named sequences, I have always imagined that the
rules for local variables would apply after elaboration.
I would like to ensure the following:
1. The scoping/visibility should be determined statically, but
probably after elaboration
2. The user should be guaranteed that if a local variable is
visible at a point in a sequence, then that variable has
been sampled, no how the sequence has been traversed in
arriving at that point.
Regarding the semantics for "||", I would like to make sure that
r; (s || t) ; u
is equivalent to
(r; s; u) || (r; t; u)
whenever both are legal.
Best regards,
John Havlicek
>
> John,
>
> I'm working with the assertion syntax working group and have a question
> about your intent with local variables. We will be discussing variable
> declaration later today and are looking at different ways of declaring
> variables in sequences and properties, these declarations should =
> reflect
> the semantics you've outlined.
>
> You've given the following example for the showing how 'x' survives
> across an intersection.
>
> sequence s6 = (
> (
> (a ; (int x = data, int y = data1) b; c)
> ||
> (d; (int x = data) (e==x))
> ) ;
> (x==data2)
> );
> // legal since x is in the intersection
>
>
> Did you intend to have this same semantic if the sequences are declared
> separately and then used hierarchically?
>
> sequence s6a = (a ; (int x = data, int y = data1) b; c);
>
> sequence s6b = (d ; (int x = data) e == x);
>
> sequence s6c = ( ( s6a || s6b ) ; ( x == data2 ) );
>
> When s6c is parsed above, there is no indication of a declaration of x,
> and this sequence would be legal or illegal given different definitions
> of s6a and s6b. In the sickest cases s6a and s6b might be hierarchical
> references or conditionally generated so that no static checking of the
> existance of any 'x' could exist until the end of elaboration.
>
> This sort of late binding is common in Verilog, but was it your
> intention to allow variables to live across separately declared
> sequences? Would you see it as useful?
>
> If it is useful, would an addition of a variable to the formal =
> arguments
> be reasonable?
> For instance (just a quick shot at syntax, not definitive):
>
> sequence s6d (output int F) = (a ; F = data, int y = data1) b; c);
> sequence s6e (output int G) = (d ; G = data) e == x);
> sequence s6f ( (int x = 0)( s6d(x) || s6e(x) )) ; (x == data2 ) );
>
> Jay
>
> =========================
> ===========
> Jay Lawrence
> Architect - Functional Verification
> Cadence Design Systems, Inc.
> (978) 262-6294
> lawrence@cadence.com
> =========================
> ===========
>
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@motorola.com]
> > Sent: Thursday, March 13, 2003 6:50 PM
> > To: sv-ac@eda.org
> > Subject: [sv-ac] revised local variable proposal
> >
> >
> > All:
> >
> > Below is a revision of the local variable proposal I sent last week.
> >
> > I have deleted the capability of getting local variables out of
> > named sequences through hierarchical references because it seems
> > to be a fringe feature that adds complexity to the semantics
> > out of proportion to the benefit provided.
> >
> > I have also changed the syntax to allow local variables to be
> > attached either to the beginning or to the end of a sequence_element.
> > This makes the definition of the sampling point convenient for the
> > user without adding any semantic complexity.
> >
> > Best regards,
> >
> > John Havlicek
> >
> > =
> =========================
> =========================
> ==================
> >
> > DISCUSSION:
> >
> > The local (i.e., dynamic) variables described in LRM 0.80 are
> > severely
> > restricted by the strict scoping rules. Since nesting of =
> implications
> > has been eliminated, it is no longer possible to attach local
> > variables
> > to the desired sampling point withing the lhs of an
> > implication. There
> > has never been a mechanism for publishing local variables outside of
> > a named subsequence or an instance thereof.
> >
> > This proposal attempts to overcome these limitations of local
> > variables
> > without separating the declaration of a local variable from
> > the sampling
> > point. The basic idea is to use a "forward flow" semantics for
> > local variables. Intuitively, once a local variable is
> > sampled, it can
> > be referenced at that or any later point of a sequence or =
> implication.
> > The definition and sampling of a local variable can be
> > attached to the
> > beginning or to the end of a sequence element.
> >
> > Thus, one can write a sequence like
> >
> > (a; !a (int x = data_in); !b*[0:inf]; b && (data_out == x))
> >
> > or an implication like
> >
> > (a; !a (int x = data_in)) => (!b*[0:inf]; b && (data_out =
> == x))
> >
> > and understand that the value sampled into x is available
> > "further to the
> > right" in the sequence or implication.
> >
> > Furthermore, one can write local variables on repeated sequences
> > and accomplish accumulation of values, as in
> >
> > (int x = 0) ((!a*[0:inf]; a (int x = x+data))*[4]; b; c &&
> > (data_out == x))
> >
> > The challenge that comes with the forward flow semantics is to
> > define which local variables are visible after a join ("or", "and",
> > "intersect"). The motivating principle in this proposal is that
> > local variables which are guaranteed to exist after the join without
> > collision can flow on, while other local variables will be lost
> > after the join.
> >
> >
> > PROPOSAL:
> >
> > This feature allows one to declare local variables and use them
> > anywhere subsequent in the property or sequence without using
> > the strict
> > scoping of 0.80 LRM.
> >
> > SYNTAX:
> >
> > BNF
> >
> > sequence_element ::=
> > "sequence_element as currently defined"
> > | `('var_decl`)' sequence_element
> > | sequence_element `('var_decl`)'
> >
> > SEMANTICS:
> >
> > 1) The declaration and assignment point of the local
> > variables is the same.
> > For example,
> >
> > sequence s1 = (a ; b (int x = data); (c==x));
> >
> > 2) There is no explicit scoping of variables related to
> > subsequences. Once
> > declared, the variable is available until the end of the
> > sequence or property.
> > For example,
> >
> > property p1 = ((a ; b (int x = data); c) => (d==x));
> >
> > 3) The local variable may be used as initializer for another
> > local variable
> > declared later in the sequence. For example,
> >
> > property p2 = ((a ; b (int x = data); c) => (1; d (int
> > x1 = x + data1); e==x1));
> >
> > 4) If a local variable is redeclared with the same name later
> > in the sequence,
> > then the later version of the variable shadows the
> > previous declaration.
> > Any reference after the redeclaraion in the sequence to
> > the variable will be
> > accessing the later declaration. Also, rhs of the
> > initialization of a variable
> > may reference a local variable with the same name, in
> > which case, the previous
> > version of the variable will be used to initialize the
> > declaration. For example,
> >
> > property p3 = ((a ; b (int x = data); c) => (1; d (int
> > x = x + data1); e==x));
> >
> > 5) There are special considerations on declaring and using
> > local variables in
> > parallel branches ("or", "and" and "intersect").
> >
> > i) Variables declared on parallel threads cannot be
> > accessed in sibling threads.
> > For example,
> >
> > sequence s4 = ((a ; (int x = data) b; c) or (d;
> > (e==x))); // this is illegal
> >
> > ii) In the case of "or", it is the intersection of the
> > variables (names)
> > that passes on past the join. All succeeding threads
> > out of "or" branches
> > continue as separate threads after the join, carrying
> > with them their
> > version of the local variables. For example,
> >
> > sequence s5 = (
> > (
> > (a ; (int x = data, int y = data1) =
> b; c)
> > ||
> > (d; (int x = data) (e==x))
> > ) ;
> > (y==data2)
> > );
> > // illegal since y is not in the intersection
> >
> > sequence s6 = (
> > (
> > (a ; (int x = data, int y = data1) =
> b; c)
> > ||
> > (d; (int x = data) (e==x))
> > ) ;
> > (x==data2)
> > );
> > // legal since x is in the intersection
> >
> > iii) In the case of "and" and "intersect", the symmetric
> > difference of the local
> > variables that were introduced in the two joining
> > threads passes on past the
> > join. In other words, each thread passes on its new
> > local variables that do
> > not appear as new local variables in the other thread.
> > A Local variable that
> > existed at the fork [i.e., at the start of the "and" or
> > "intersect"] of
> > the two threads is passed on provided that it was not
> > overwritten in either
> > of the joining threads. Since only the difference of
> > the new variables is
> > passed on, the two joining threads are merged into one
> > thread at the join.
> >
> > sequence s7 = (
> > (
> > (a ; (int x = data, int y = data1) =
> b; c)
> > &&
> > (d; (int x = data) (e==x))
> > ) ;
> > (x==data2)
> > );
> > // illegal since x common to both threads
> >
> > sequence s8 = (
> > (
> > (a ; (int x = data, int y = data1) =
> b; c)
> > &&
> > (d; (int x = data) (e==x))
> > ) ;
> > (y==data2)
> > );
> > // legal since y is in the difference
> >
> >
> > iv) The intersection and difference of the sets of names
> > should be computed
> > statically at compile time.
> >
This archive was generated by hypermail 2b28 : Mon Mar 17 2003 - 08:17:51 PST