FINAL PROPOSAL, 12-DEC-2003

SVA 3.1A PROPOSAL 19:  ATTACHING TASKS TO SEQUENCE MATCHES
----------------------------------------------------------

DISCUSSION:

Because local variables cannot be referenced in the action blocks of
3.1 assertions, the action blocks are inadequate for error reporting
or other post-evaluation processing of an assertion.  This situation
leaves open a serious hole in the usability features of the language.

It has been a goal of the 3.1a effort for some time to find a way to
access local variables from a property in its associated action
blocks.  We have been unable to find a good solution to this problem
becuase of the multiple threading in a single assertion attempt and
the fact that distinct threads evolve to acquire distinct local
variable contexts.

This proposal compensates for the inability to reference local
variables in the action blocks by allowing tasks and system tasks to
be called at the end of successful match of a sequence.  The syntax is
to put the task calls in the comma-separated list along with local
variable assignments.  Such a task or system task call can be passed
local variables that flow out of the match of the sequence as well as
any local variables assigned in the comma-separated list prior to the
task call.  All arguments to such a task must be inputs and must be
passed by value.

By encapsulating within a task the code that would have been put in the 
action blocks, much of the desired capability for the action blocks
is achieved on the match of the 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 {, sequence_match_item } ) [ boolean_abbrev ] 
        | sequence_instance [ sequence_abbrev ] 
        | ( sequence_expr {, sequence_match_item } ) [ 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 

     sequence_match_item ::=
          variable_assignment
        | task_enable
        | system_task_enable
        

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 {, sequence_match_item } ) [ boolean_abbrev ] 
        | sequence_instance [ sequence_abbrev ] 
        | ( sequence_expr { , sequence_match_item } ) [ 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 {, sequence_match_item } ) [ boolean_abbrev ] 
        | ( sequence_expr { , sequence_match_item } ) [ 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 {, sequence_match_item } ) [ boolean_abbrev ] 
        | sequence_instance [ sequence_abbrev ] 
        | ( sequence_expr {, sequence_match_item } ) [ 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 

     sequence_match_item ::=
          variable_assignment
        | task_enable
        | system_task_enable


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

p. 174.  Add the following section between sections 17.8 and 17.9.
Sections 17.9 and later therefore also need to be renumbered.

17.?  Calling tasks and system tasks on match of a sequence

Tasks and system tasks can be called at the end of successful match of
a sequence or subsequence.  The task calls, like local variable
assignments, are put in the comma-separated list that follows the
sequence, and the sequence followed by the list are enclosed in
parentheses.  

[begin syntax box]

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

     sequence_match_item ::=
          variable_assignment
        | task_enable
        | system_task_enable

[end syntax box]

For example, 

   sequence s1;
      logic v;
      (a, v=e) ##1 (b, $display("b following a with v sampled as %h", v));
   endsequence

causes the system task $display to be executed on successful match
of b.  

Local variables can be passed into tasks and system tasks that are 
called at the end of a sequence.  Any local variable that flows 
out of the sequence or that is assigned in the list following the
sequence before the task call can be used in an actual argument 
expression for the task.

All arguments of a task or system task called at the end of successful
match of a sequence must be inputs and must receive their actual
arguments by value.


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

None.  The task and system task calls do not affect the formal semantics
of the sequence.