DRAFT, 3-NOV-2003

SVA 3.1A PROPOSAL:  ACCESSING LOCAL VARIABLES
---------------------------------------------

DISCUSSION:
-----------

SVA 3.1 already provides for access of local variables sampled within
a defined sequence in the instantiating context of an instance of the
sequence.  The mechanism is to define the local variables in the
instantiating context and pass them into the instance as actual
arguments.  Provided the local variables flow out of the definition of
the instantiated sequence, they can be accessed later in the
instantiating context.

SVA 3.1 forbids passing arguments to a sequence to which "ended" or
"matched" is applied, requiring instead that the desired instance with
actual arguments be embedded within an auxiliary defined sequence that
has no arguments.  As a result, local variables cannot be passed out
of applications of "ended" or "matched".

This proposal relaxes the restriction on passing local variables to
sequence instances to which "ended" or "matched" is applied and allows
local variables to flow out of such an instance.

Passing local variables in
--------------------------

This proposal allows local variables in the instantiating context
to be passed into an instance of a defined sequence to which "ended"
or "matched" is applied provided the following restriction is met:

   RESTRICTION: If "ended" or "matched" is applied to any instance
   of a defined sequence S and if S has a local variable v as formal
   argument, then v must not be referenced within the definition of S
   before it is sampled within S.  In particular, if "v = exp" is a
   sampling of v in the definition of S and if v has not been
   previously sampled in S, then v cannot be in the support of "exp".

The effect of this restriction is that the values of local variables 
sampled outside do not flow into an instance of such a sequence.


EXAMPLE 1:  Here is an example that violates the restriction.

   sequence s(a);
      a ##1 (!b)[*3] ##1 (c == a);
   endsequence

   property p;

      [0:0] x;
      (d, x = expr) ##1 s(x).ended |=> e ;

   endproperty

Notice that the first reference to "a" in sequence s is four cycles prior 
to the end of the sequence.  Therefore, in property p, "x" has not even 
been sampled at this time.

////

EXAMPLE 2:  Here is an example that satisfies the restriction.

   sequence s(a);
      (c1, a = expr1) ##1 (!b)[*3] ##1 (c == a);
   endsequence

   property p;

      [0:0] x;
      (d, x = expr) ##1 s(x).ended |=> e ;

   endproperty

Since "a" is sampled before it is referenced in sequence s, 
the use of "s(x).ended" in property p is legal.  Notice that 
the value of expr sampled into x is not used in sequence s.

////

Getting local variables out
---------------------------

A local variables that is passed in as actual argument to an 
instance of a defined sequence to which "ended" or "matched" 
is applied will flow out of that instance in the instantiating
context provided both of the following conditions are met:

1. The local variable flows out of the end of the defined 
   sequence instance, as defined by the local variable flow 
   rules for sequences.

2. The application of "ended" or "matched" to this instance is
   a maximal boolean expression.  In other words, the application
   of "ended" or "matched" cannot have boolean negation or any 
   other boolean expression operator applied to it.

If both conditions are met, then the value that flows out of
the end of the defined sequence instance is treated as though
it were sampled in the instantiating context at the point of
the application "ended" or "matched".


EXAMPLE 3:  Here is an example that does not satisfy the second
condition.

   sequence s(a);
      (c1, a = expr1) ##1 (!b)[*3] ##1 (c == a);
   endsequence

   property p;

      [0:0] x;
      (d, x = expr) ##1 (t && !s(x).ended) |=> (e == x) ;

   endproperty

In this case, the value of expr sampled into x is the one that
is used in the comparison "e == x".

////

EXAMPLE 4:  Here is an example that satisfies both conditions.

   sequence s(a);
      (c1, a = expr1) ##1 (!b)[*3] ##1 (c == a);
   endsequence

   property p;

      [0:0] x;
      (d, x = expr) ##1 s(x).ended |=> (e == x) ;

   endproperty

In this case, the value of expr1 sampled into a in sequence s
is the one that is used in the comparison "e == x".

////


In a single cycle, there can be multiple matches of a sequence
instance to which "ended" is applied and these matches can have
different valuations of the local variables.  The multiple matches are
treated semantically the same way as matching both disjuncts of an
"or".  In other words, the thread evaluating the instance to which
"ended" is applied will fork to account for such distinct
local variable valuations.

Such forking occurs analogously when a multi-clocked sequence
evaluates a sequence instance to which "matched" is applied.  In this
case, the multiple matches that result in forking need not be
simultaneous, but they all must occur strictly before the clock event
in the instantiating context at which the application of "matched" is
evaluated.


SEMANTICS
---------

T(V) denotes an instance of a clocked or unclocked sequence that is
passed the local variables V as actual arguments

* w^j,L_0,L_1 |== T(V).ended iff there exist 0 <= i <= j 
  and L such that both w^{i,j},{},L |== T(V) and 

     L_1 = L_0 |_{dom(L_0) - (dom(L) \cap V)} \cup L|_V

* w^j,L_0,L_1 |= @(c) (T(V).matched) iff there exists 0 <= i < j 
  such that w^i,L_0,L_1 |= T(V).ended and 
  w^{i+1,j},{},{} |== (!c[*0:$] ##1 c).