Subject: [sv-ac] local variable proposal
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Mar 20 2003 - 07:46:32 PST
All:
Below is a revision of the "forward flow" local variable
proposal. Here are the changes:
1. New rule for "&&" and "intersect" as suggested by Erich Marschner.
This rule now allows a local variable that exists before the fork and
is sampled in exactly one branch of the "&&" or "intersect" to pass
on with its latest sampled value.
2. Rewrote the rules for "||", "&&", "intersect" to try to make them
clearer.
3. Changed "and" to "&&", "or" to "||" in a few places.
This proposal does not address the issues discussed with Jay Lawrence
about local variables flowing into and out of instances of named
sequences. As you have seen in my previous mail, I was being naive
in saying that the rules below should apply after elaboration of
named sequence instances. Such a convention will make the namespaces
of defined sequences difficult to manage.
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 an "||", "&&",
or "intersect". The motivating principle in this proposal is that
local variables which are guaranteed to exist after such an operation
without collision can flow on, while other local variables will be lost.
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 ("||", "&&" and "intersect").
i) Variables declared on parallel threads cannot be accessed in sibling threads.
For example,
sequence s4 = ((a ; (int x = data) b; c) || (d; (e==x))); // this is illegal
ii) In the case of "||", it is the intersection of the variables (names)
that passes on past the "||". More precisely, a local variable passes
on past the "||" iff either
a. The local variable exists at the start of the "||".
or
b. The local variable is sampled in both branches of the "||".
Note that both a. and b. can hold. All succeeding threads out of "||"
branches continue as separate threads, carrying with them their
own latest samplings of the local variables. These threads do not
have to have consistent valuations for 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 "intersect", the symmetric difference of the
local variables that are sampled in the two joining threads passes on
past the join. More precisely, a local variable passes on past the
join iff either
a. The local variable exists at the start of the "&&" or "intersect"
and is sampled in neither branch.
or
b. The local variable is sampled in exactly one of the branches.
The value passed on is the latest sampled value. 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 : Thu Mar 20 2003 - 07:47:14 PST