Subject: [sv-ac] local variables
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Mar 05 2003 - 13:33:09 PST
All:
Below is a draft proposal for enhancing local variables in SVA.
I am sending it now to get it in before the freeze tomorrow.
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.
Thus, one can write a sequence like
(a; (int x = data_in) !a; !b*[0:inf]; b && (data_out == x))
or an implication like
(a; (int x = data_in) !a) => (!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]; (int x = x+data)a)*[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.
This proposal also introduces a hierarchical reference syntax for
accessing local variables at the end of a named sequence. There is
a challenge associated with this feature, namely to define what
happens when multiple matches of the named sequence occur at the
same time. This situation can result in multiple copies of the
referenced local variable with inconsistent values. The proposed
semantics is to fork on such multiple matches, but to universally
quantify over the various forked threads.
JH: This proposed semantics should be scrutinized. My intuition
JH: is that for the purpose of defining tight satisfaction,
JH: such multiple match situations should be existentially
JH: quantified.
JH:
JH: The proposed syntax does not deal with the situation in which
JH: a named sequence is instantiated as a subsequence of another
JH: sequence or implication.
PROPOSAL:
Two major enhancements have been made to the local variable feature,
compared to this feature as described in LRM 0.80.
a) This feature allows to declare local variables and use them
anywhere in the property or sequence without using the strict scoping
of 0.80 LRM.
b) It allows accessing local variables from a named sequence when the
named sequence is used in a property or another sequence.
SYNTAX:
BNF
sequence_expr ::=
"sequence_expr as currently defined"
| (var_decl) sequence_expr
sequence_phrase ::=
"sequence_phrase as currently defined"
| (var_decl) sequence_phrase
boolean_expr_var replaces boolean_expr in the previous BNF from the LRM 0.80
SEMANTICS:
A. Declaring and using local variable
1) The declaration and assignment point of the local variables is the same.
For examle,
sequence s1 = (a ; (int x = data) b; (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 ; (int x = data) b; 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 ; (int x = data) b; c) => ((int x1 = x + data1) (d==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 be used to initialize the declaration. For example,
property p3 = ((a ; (int x = data) b; c) => ((int x = x + data1) (d==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)
or
(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)
or
(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. Since only the
difference is passed on, there is only one thread continuing even if there
were more than one thread that reached the join at the same time.
sequence s7 = (
(
(a ; (int x = data, int y = data1) b; c)
and
(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)
and
(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.
B. Accessing local variables of named sequences
6) Local variables declared within a sequence can accessed in another sequence via
hierarchical naming, seq_name.var_name. For example,
sequence s9 = (a ; (int x = data, int y = data1) b; c);
sequence s10 = (d ; e; (s9.x == data2));
7) The sequence must end at the point where the value is accessed. Otherwise, the
comparison of such a variable will result in false. For example, in s10, if
sequence s9 doesn't end where s9.x is used, then (s9.x == data2) will be false,
regardless of the value of data2.
8) If there are multiple matches where the variable is accessed, then
separate attempts are forked off at that point, corresponding to each
match. Each forked branch acts independent of the other and uses the
value of the variable from its corresponding match.
sequence s11 = (a ; (int x = data, int y = data1) b; ([1:2]c));
property p12 = (d ; e; (s11.x == data2));
It is possible that there are two matches simultaneously for c at the end of
sequence s11. Let's say, the values of x are v1 and v2 for the two matches.
Then p12 becomes:
property p12_v1 = (d ; e; (v1 == data2));
property p12_v2 = (d ; e; (v2 == data2));
Both properties p12_v1 and p12_v2 must hold.
This archive was generated by hypermail 2b28 : Wed Mar 05 2003 - 13:38:24 PST