Subject: RE: [sv-ac] revised local variable proposal
From: Jay Lawrence (lawrence@cadence.com)
Date: Mon Mar 17 2003 - 06:27:20 PST
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 - 06:28:04 PST