DRAFT, 2-NOV-2003

SVA 3.1A PROPOSAL:  PROPERTY CONJUNCTION
----------------------------------------

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

This proposal extends the SVA language by allowing boolean conjunction
of property expressions as a property expression.  The syntax of the 
boolean conjunction operator is "and".

The need for conjunction of properties arises when a single
precondition obligates all of several consequents.  In SVA 3.1, the
property forms are so limited that sequence conjunction is generally
adequate.

The current proposal enhances the usefulness of the proposals on
generalized implication and property instances.


EXAMPLE:  If the proposal on generalized implication passes,
then instead of coding two separate property expressions

   (s1 |=> (s2 ## s3))

and

   (s1 |=> (s4 |=> s5))

which tends to hide the fact that the antecedent is shared, the 
user can combine them into one property expression

   (
      s1 
      |=> 
      (
         (s2 ## s3)
         and
         (s4 |=> s5)
      )
   )

////

This proposal is in alignment with proposed Accellera PSL 1.1.


SEMANTICS
---------

1. Unclocked Semantics.

      w |= p1 and p2  iff  w |= p1 and w |= p2

   In the presence of local variables:

      w,L |= p1 and p2  iff  w,L |= p1 and w,L |= p2

2. Clock Rewrite Rule.

      @(c)(p1 and p2)  |-->  (@(c) p1 and @(c) p2)



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

Differently clocked property expressions can be combined with "and" to
yield a multiply-clocked property expression.  Multiply-clocked
property expressions can be combined with "and" to yield a
multiply-clocked property expression.

If p1 and p2 have the same leading clock, then it is the leading clock
of "p1 and p2".  Otherwise the leading clock of "p1 and p2" is UNCERTAIN.


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

[TBD.  Depends on the combination of proposals that pass.
Should be developed from a subset of the changes in the 
original combined proposal.]


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

[TBD.  Depends on the combination of proposals that pass.
Should be developed from a subset of the changes in the 
original combined proposal.]
   

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

[TBD.  Depends on the combination of proposals that pass.
Should be developed from a subset of the changes in the 
original combined proposal.]