DRAFT, 23-NOV-2003

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

DISCUSSION:

In SVA 3.1, local variable sampling can be attached only to a boolean
expression.
        
This proposal 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.

The syntax is

   ( sequence_expr , identifier = expression )


EXAMPLE:  As an alternative to

   (r1 and r2) ##0 (1'b1, v = e)

one can code

   (r1 and r2, v = e)

////


SEMANTICS
---------

"(sequence_expr, v = e)" is a derived form, semantically equivalent to
"sequence_expr ##0 (1'b1, v = e)".


MULTIPLE CLOCK SUPPORT
----------------------

This proposal does not change the multiple clock support for local 
variables.

Sampling of local variables occurs within a singly-clocked sequence,
although the local variables can flow out of that sequence.


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

p. 150, box 17-2.  Change

     sequence_expr ::=                                    // from Annex A.2.10
          cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } 
        | sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } 
        | expression { , function_blocking_assignment } [ boolean_abbrev ] 
        | ( expression {, function_blocking_assignment } ) [ boolean_abbrev ] 
        | sequence_instance [ sequence_abbrev ] 
        | ( sequence_expr ) [ sequence_abbrev ] 
        | sequence_expr and sequence_expr 
        | sequence_expr intersect sequence_expr 
        | sequence_expr or sequence_expr 
        | first_match ( sequence_expr ) 
        | expression throughout sequence_expr 
        | sequence_expr within sequence_expr 

   to

     sequence_expr ::=                                    // from Annex A.2.10
          cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } 
        | sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } 
        | expression [ boolean_abbrev ] 
        | ( expression {, function_blocking_assignment } ) [ boolean_abbrev ] 
        | sequence_instance [ sequence_abbrev ] 
        | ( sequence_expr {, function_blocking_assignment } ) [ sequence_abbrev ] 
        | sequence_expr and sequence_expr 
        | sequence_expr intersect sequence_expr 
        | sequence_expr or sequence_expr 
        | first_match ( sequence_expr ) 
        | expression throughout sequence_expr 
        | sequence_expr within sequence_expr 


p. 155, box 17-5.  Change


     sequence_expr ::=                                    // from Annex A.2.10
        ...
        | expression { , function_blocking_assignment } [ boolean_abbrev ] 
        | ( expression {, function_blocking_assignment } ) [ boolean_abbrev ] 
        | sequence_instance [ sequence_abbrev ] 
        | ( sequence_expr ) [ sequence_abbrev ] 
        ...

   to

     sequence_expr ::=                                    // from Annex A.2.10
        ...
        | expression [ boolean_abbrev ] 
        | ( expression {, function_blocking_assignment } ) [ boolean_abbrev ] 
        | sequence_instance [ sequence_abbrev ] 
        | ( sequence_expr { , function_blocking_assignment } ) [ sequence_abbrev ] 
        ...

p. 172, box 17-13.  Change


     sequence_expr ::=                                    // from Annex A.2.10
        ...
        | expression { , function_blocking_assignment } [ boolean_abbrev ] 
        | ( expression {, function_blocking_assignment } ) [ boolean_abbrev ] 

   to

     sequence_expr ::=                                    // from Annex A.2.10
        ...
        | ( expression {, function_blocking_assignment } ) [ boolean_abbrev ] 
        | ( sequence_expr { , function_blocking_assignment } ) [ sequence_abbrev ] 
        ...

p. 280.  Change

     sequence_expr ::=                                    // from Annex A.2.10
          cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } 
        | sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } 
        | expression { , function_blocking_assignment } [ boolean_abbrev ] 
        | ( expression {, function_blocking_assignment } ) [ boolean_abbrev ] 
        | sequence_instance [ sequence_abbrev ] 
        | ( sequence_expr ) [ sequence_abbrev ] 
        | sequence_expr and sequence_expr 
        | sequence_expr intersect sequence_expr 
        | sequence_expr or sequence_expr 
        | first_match ( sequence_expr ) 
        | expression throughout sequence_expr 
        | sequence_expr within sequence_expr 

   to

     sequence_expr ::=                                    // from Annex A.2.10
          cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } 
        | sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } 
        | expression [ boolean_abbrev ] 
        | ( expression {, function_blocking_assignment } ) [ boolean_abbrev ] 
        | sequence_instance [ sequence_abbrev ] 
        | ( sequence_expr {, function_blocking_assignment } ) [ sequence_abbrev ] 
        | sequence_expr and sequence_expr 
        | sequence_expr intersect sequence_expr 
        | sequence_expr or sequence_expr 
        | first_match ( sequence_expr ) 
        | expression throughout sequence_expr 
        | sequence_expr within sequence_expr 


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

p. 172, after box 17-13.  Change

      The type of variable is explicitly specified. The variable can
      be assigned anywhere in the sequence and reassigned later in
      the sequence. For every attempt, a new copy of the variable is
      created for the sequence. The variable value can be tested like
      any other SystemVerilog variable.

   to

      The type of variable is explicitly specified. The variable can
      be assigned at the end point of any syntactic subsequence by
      placing the subsequence, comma separated from the sampling
      assignment, in parentheses.  For example, if in 

         a ##1 first_match(b) ##1 c[*2]

      it is desired to sample x = e at the first match of b, the sequence 
      expression can be rewritten as

         a ##1 (first_match(b), x = e) ##1 c[*2]

      The local variable can be reassigned later in the sequence, as in 

         a ##1 (first_match(b), x = e) ##1 (c[*2], x = x + 1)

      For every attempt, a new copy of the variable is created for the
      sequence. The variable value can be tested like any other
      SystemVerilog variable.
         

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

p. 346, line 3.  Change

      * ( b, v = e ) \equiv ( b ##0 ( 1, v = e )) .
      * ( 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 ) ) for k > 1 .
 
   to

      * ( R, v = e ) ( R ##0 ( 1, v = e )) .
      * ( 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 ) ) for k > 1 .
