FINAL PROPOSAL, 5-DEC-2003

SVA 3.1A PROPOSAL 03:  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 restrictions are met:

   RESTRICTION 1:  Local variables passed into an instance of a defined
   sequence to which "ended" or "matched" is applied must be passed as
   entire actual arguments, not as proper subexpressions of actual 
   arguments.

   RESTRICTION 2: If "ended" or "matched" is applied to an instance of
   a defined sequence S and if a local variable is passed as actual
   argument to the formal argument v of S, 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 these restrictions 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 Restriction 2.

   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 both restrictions.

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


=========================================================================
PROPOSED LRM CHANGES
=========================================================================


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

None.


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

*. p. 168, before section 17.7.11.  Change

      ended can be used directly on sequences that do not have formal
      arguments.  To use ended on a sequence with arguments, first
      define a sequence without formal arguments that instantiates the
      sequence with actual arguments.  For example,
      
         sequence e2(a,b,c); 
            @(posedge sysclk) $rose(a) ##1 b ##1 c; 
         endsequence
         sequence e2_instantiated; 
            e2(ready,proc1,proc2); 
         endsequence
         sequence rule2; 
            @(posedge sysclk) reset ##1 inst ##1 e2_instantiated.ended ##1 branch_back; 
         endsequence

   to 

      ended can be used on sequences that have formal arguments.  For
      example with the definitions

         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

      rule2 is equivalent to rule2a below:

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

      There are additional restrictions on passing local variables into
      an instance of a sequence to which ended is applied.  See Section 17.8.


*. p. 173, before the paragraph beginning "Note that when a local variable is a 
   formal argument".  Add

      Local variables can be passed into an instance of a defined
      sequence to which ended is applied and accessed in a similar
      manner.  For example

         sequence seq2a; 
            int v1; c ##1 sub_seq2(v1).ended ##1 (do1 == v1); // v1 is now bound to lv
         endsequence

      There are additional restrictions when passing local variables 
      into an instance of a defined sequence to which ended is applied:  

      1. Local variables can be passed in only as entire actual
         arguments, not as proper subexpressions of actual arguments.
 
      2. In the declaration of the defined sequence, the formal argument
         to which the local variable is bound must not be referenced
         before it is sampled.

      The second restriction is met by sub_seq2 because the sampling 
      lv = data_in occurs before the reference to lv in data_out == lv.

      If a local variable is sampled before being passed into an
      instance of a defined sequence to which ended is applied, then
      the restrictions prevent this sampled value from being visible
      within the defined sequence.  The restrictions are important
      because the use of ended means that there is no guaranteed
      relationship between the point in time at which the local
      variable is sampled outside the defined sequence and the
      beginning of the match of the instance.

      A local variable that is passed in as actual argument to an
      instance of a defined sequence to which ended is applied will
      flow out of the application of ended to that instance provided
      both of the following coditions 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.  (See below and Annex G.)
      
      2. The application of ended to this instance is a maximal boolean 
         expression.  In other words, the application of ended cannot 
         have negation or any other expression operator applied to it.

      Both conditions are satisfied by sub_seq2 and seq2a.  Thus, in seq2a
      the value in v1 in the comparison do1 == v1 is the value sampled 
      into lv in sub_seq2 by the assignment lv = data_in.  However, in 

         sequence seq2b; 
            int v1; c ##1 !sub_seq2(v1).ended ##1 (do1 == v1); // v1 undefined
         endsequence
   
      the second condition is violated because of the negation applied
      to sub_seq2(v1).ended.  Therefore, v1 does not flow out of the
      application of ended to this instance, and so the reference to
      v1 in do1 == v1 is to an unsampled variable.
            
      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 (see below).  In other words, the thread
      evaluating the instance to which ended is applied will fork to
      account for such distinct local variable valuations.


*. p. 179, before 17.12.  Change

      Like ended, matched can be used directly on sequences that do not have
      formal arguments.
      
      An example is shown below:
      
         sequence e1; 
            @(posedge clk) $rose(ready) ##1 proc1 ##1 proc2 ; 
         endsequence
         sequence e2; 
            @(posedge sysclk) reset ##1 inst ##1 e1.matched [*->1] ##1 branch_back; 
         endsequence
      
      In this example, source sequence e1 is evaluated at clock clk, while
      the destination sequence e2 is evaluated at clock sysclk. In e2, the
      end point of e1 is tested to occur sometime after the occurrence of
      inst. Notice that method matched only tests for the end point of e1
      and has no bearing on the starting point of e1.

   to

      Like ended, matched can be used on sequences that have formal arguments.
      
      An example is shown below:
      
         sequence e1(a,b,c); 
            @(posedge clk) $rose(a) ##1 b ##1 c; 
         endsequence
         sequence e2; 
            @(posedge sysclk) reset ##1 inst ##1 e1(ready,proc1,proc2).matched [*->1] ##1 branch_back; 
         endsequence
      
      In this example, source sequence e1 is evaluated at clock clk,
      while the destination sequence e2 is evaluated at clock
      sysclk. In e2, the end point of the instance
      e1(ready,proc1,proc2) is tested to occur sometime after the
      occurrence of inst. Notice that method matched only tests for
      the end point of e1(ready,proc1,proc2) and has no bearing on the
      starting point of e1(ready,proc1,proc2).

      Local variables can be passed into an instance of a defined
      sequence to which matched is applied.  The same restrictions
      apply as in the case of ended.  Values of local variables
      sampled in an instance of a defined sequence to which matched is
      applied will flow out under the same conditions as for ended.
      See Section 17.8.

      As with ended, a sequence instance to which matched is applied
      can have multiple matches in a single cycle of the destination
      sequence clock.  The multiple matches are treated semantically
      the same way as matching both disjuncts of an "or".  In other
      words, the thread evaluating the destination sequence will fork
      to account for such distinct local variable valuations.



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

p. 351, beginning of the section on extended booleans.  Change

      w denotes a non-empty finite or infinite word over \Sigma, j denotes
      an integer such that 0 <= j < |w|, and T denotes a clocked or
      unclocked sequence.
      
      * w^j |= T.ended iff there exist 0 <= i <= j and L such that 
        w^{i,j},{},L |== T.
      
      * 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 denotes a non-empty finite or infinite word over \Sigma, j denotes
      an integer such that 0 <= j < |w|, and 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).
