Subject: [sv-ac] revised local variable proposal
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Mar 13 2003 - 15:50:25 PST
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 : Thu Mar 13 2003 - 15:55:20 PST