DRAFT, 3-NOV-2003

SVA 3.1A PROPOSAL:  ACCESSING AND SAMPLING 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.  This effectively prevents sampled values of local
variables from being passed into the instance.  This restriction is
sensible because the temporal relationship of the sampling point of
such local variables to the beginning of a match of the sequence to
which "ended" or "matched" is applied is unkown.  However, the
restriction is more severe than necessary and has the effect of
preventing local variables from passing 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.  This
allows local variable values sampled within such instances to be
accessed in the intantiating context by the same mechanism as that for
ordinary sequence instances.  The following restriction is imposed,
though, in order to avoid passing sampled values of local variables
into a sequence instance to which "ended" or "matched" is applied:

   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 or initialized in S, then v cannot be in the
   support of "exp".

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

In a single cycle, there can be mutliple 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" 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 before the clock event that
leads the subsequence that follows the evaluation.

This proposal also makes coding of the sampling of local variables
simpler by allowing sampling to occur after any sequence expression,
not just booleans.  This extension is an abbreviation for a capability
that already exists in the language, as

   (sequence_expr, v = e)

is semantically equivalent to 

   sequence_expr ##0 (1'b1, v = e)

Thus, as an alternative to

   (!a[*0:$] ##1 (a, v = e) ##1 first_match(##[0:$]b) |=> c

one can code

   (first_match(##[0:$]a), v = e) ##1 first_match(##[0:$]b) |=> c


This proposal does not provide for access of local variables in the
action block.  The capability needed to generated error messages
with local variables seems better solved by moving the activation
of the messages into the assertion definitions rather than trying
to solve the problem of accomodating multiple threads with distinct
local variable valuations in a single execution of the action block.
   

PROPOSED CHANGES TO THE BNF:
----------------------------

1. p. 155, box 17-5.  Change

      sequence_expr ::=
         ...
         | expression { , function_blocking_assignment } [boolean_abbrev]
         | (expression { , function_blocking_assignment } ) [boolean_abbrev]
         | sequence_instance [ sequence_abbrev ]
         | (sequence_expr) [ sequence_abbrev ]

   to

      sequence_expr ::=
         ...
         | expression
         | sequence_expr { , function_blocking_assignment } [boolean_abbrev]
         | (sequence_expr { , function_blocking_assignment } ) [boolean_abbrev]
         | sequence_instance [ sequence_abbrev ]
         | (sequence_expr) [ sequence_abbrev ]

2. p. 172, box 17-13.  Change

      sequence_expr ::=
         ...
         | (expression { , function_blocking_assignment } ) [boolean_abbrev]
         | expression { , function_blocking_assignment } [boolean_abbrev]
   to

      sequence_expr ::=
         ...
         | sequence_expr { , function_blocking_assignment } [boolean_abbrev]
         | (sequence_expr { , function_blocking_assignment } ) [boolean_abbrev]

3. p. 281, in the production for sequence_expr.  Change 

         | expression { , function_blocking_assignment } [boolean_abbrev]
         | (expression { , function_blocking_assignment } ) [boolean_abbrev]

   to

         | expression
         | sequence_expr { , function_blocking_assignment } [boolean_abbrev]
         | (sequence_expr { , function_blocking_assignment } ) [boolean_abbrev]


PROPOSED CHANGES TO LRM TEXT:
-----------------------------

1. 17.7.10, p. 168.  Change

      ended can be used directly ... <to the end of the subsection>

   to

      ended can be used on an instance of a defined sequence with 
      arguments.  For example,

         sequence e2(a,b,c);
            @(posedge sysclk) $rose(a) ##1 b ##1 c;
         endsequence

         sequence rule2;
            @(posedge sysclk) 
            reset ##1 inst ##1 e2(ready,proc1,proc2).ended ##1 branch_back;
         endsequence

      If ended is applied to an instance of a defined sequence with
      formal arguments, then for any formal argument that is a local
      variable (17.8), the local variable must be sampled in the
      definition of the sequence before it can be referenced.

2. 17.8, p. 172, before "Local variables can be written on repeaded 
   sequences and accomplish accumulation of values".     Add

      Local variables can be sampled at the end of any sequence expression.
      For example, 

         sequence two_cycle_stability;
            [7:0] x;
            ($first_match(##[0:$]req), x = attribute) 
            ##1 (a && (attribute == x));
         endsequence

3. 17.8, p. 173, before "There are special considerations on using
   local variables in parallel branches ...".  Add
 
      Also, if a local variable is a formal argument of a sequence
      to which "ended" is applied, then in the definition of the 
      sequence the local variable must be sampled before it can be
      referenced.

4. 17.11, p. 179.  Delete

      Like ended, matched can be used directly on sequences that do 
      not have formal arguments.

5. 17.11, p. 179, end of subsection.  Add,

      If a local variable is a formal argument of a sequence
      to which "matched" is applied, then in the definition of the 
      sequence the local variable must be sampled before it can be
      referenced.

6. [TBD.  Add some intuitive discussion of getting local variables
   out of an instance to which "matched" is applied and give an 
   example.]

PROPOSED CHANGES TO THE FORMAL SEMANTICS:
-----------------------------------------

1. G.2.3.5, p. 346.  Change

      * (b, v = e)  \equiv  (b ##0 (1, v = e))

   to

      * (R, v = e)  \equiv  (R ##0 (1, v = e))

2. G.2.3.5, p. 346.  Change

      * (b, v_1 = e_1,..., v_k = e_k)  \equiv  
        ( (b, v_1 = e_1) ##0 (1, v_2 = e_2,..., v_k = e_k) )

   to

      * (R, v_1 = e_1,..., v_k = e_k)  \equiv  
        ( (R, v_1 = e_1) ##0 (1, v_2 = e_2,..., v_k = e_k) )

3. G.4.1, p. 351.  Change

      T denotes a clocked or unclocked sequence

   to 

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

4. G.4.1, p. 351.  Change

      * w^j |= T.ended iff there exist 0 <= i <= j and L such that 
        w^{i,j},{},{} |== T

   to

      * 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

5. G.4.1, p. 351.  Change

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

   to 

      * 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).