Subject: Re: [sv-ac] revised local variable proposal
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Mar 19 2003 - 13:48:53 PST
Jay:
Kurt Shultz and I have been thinking some more about SVA local
variables going into and coming out of instances of named sequences.
I said the local variable semantics should probably apply after
elaboration, but we are now concerned about namespace issues that
I hadn't thought so clearly about before.
Kurt has pointed out concern about "pollution" out of an
instance of a named sequence. It seems like a good idea to
be able to define what local variables get published out of
an instance of a named sequence, something like your "output"
syntax, and to support a reasonable mechanism for binding published
variables to new names in the instantiating context.
The non-published variables would not be visible outside the
named sequence.
Regarding the flow of local variables into an instance of a named
sequence, I think the preferred way would always be through the
parameter list of the sequence. Should the namespace of the
named sequence definition be protected so that an instance
cannot pick up a local variable that is not passed in as a
parameter?
Best regards,
John Havlicek
> Date: 17 Mar 2003 10:13:04 -0600
> CC: john.havlicek@motorola.com, sv-ac@eda.org
> From: John Havlicek <john.havlicek@motorola.com>
> Reply-to: john.havlicek@motorola.com
>
> 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 : Wed Mar 19 2003 - 13:50:19 PST