DRAFT, 2-NOV-2003

SVA 3.1A PROPOSAL:  CLOCK FLOW
------------------------------

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

In SVA 3.1, the rules governing the specification of clocks for
multiply-clocked sequence and property expressions are overly
restrictive.  In the case of singly-clocked sequences and properties,
great flexibility is afforded in how the clock can be specified.
However, if a multiply-clocked sequence or property expression is
defined, then its components must all be explicitly clocked.  This
means that even if the clock does not change over an operator such as
"##" and "|=>", the clock event must be specified redundantly.

For example, in SVA 3.1

   @(c) r1 |=> r2 

is legal as a singly-clocked property expression and is equivalent to

   @(c) r1 |=> @(c) r2,

but 

   @(d) r0 ## @(c) r1 |=> r2

is no longer legal due to the restrictions in the multiple clock support.
This property expression must be rewritten with explicit specification 
of the clock on r2 as

   @(d) r0 ## @(c) r1 |=> @(c) r2

This proposal provides that the prevailing clock shall flow through
operators from left to right and shall govern the righthand operands
except in the case that the operator is one after which the clock can
be changed (currently limited to "##" and "|=>") and the new clock
appears explicitly on the righthand side of the operator.  Thus, under
this proposal,

   @(d) r0 ## @(c) r1 |=> r2

will be legal and will be equivalent to 

   @(d) r0 ## @(c) r1 |=> @(c) r2
 
due to the flow of "@(c)" through "|=>", while the meaning of 

   @(d) r0 ## @(c) r1 |=> @(e) r2

will be unchanged.  


SEMANTICS
---------

No change to the formal semantics is needed provided clocking is made
explicit before applying the formal semantics.
  

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

[TBD.  Depends on the combination of proposals that pass.]


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

[TBD.  Depends on the combination of proposals that pass.]
   

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

[TBD.  Depends on the combination of proposals that pass.]