DRAFT, 2-NOV-2003

SVA 3.1A PROPOSAL:  PROPERTY DISJUNCTION
----------------------------------------

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

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

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

In my opinion, the need for general (non-deterministic, non-exclusive)
property disjunction is less than the need for property conjunction
and "if-else" combination of properties.  

However, this proposal is needed if both the proposals on property
conjunction and property negation pass, since they will enable the
user to derive property disjunction in the usual way

   p1 or p2  \equiv  not((not p1) and (not p2))

In that case, the current proposal gives the more convenient syntax
of the lefthand side.

EXAMPLE:  If the proposal on generalized implication passes,
then the user can combine consequents of an implication by 
disjunction:

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

////

This proposal is in alignment with proposed Accellera PSL 1.1.


SEMANTICS
---------

1. Unclocked Semantics.

      w |= p1 or p2  iff  w |= p1 or w |= p2

   In the presence of local variables:

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

2. Clock Rewrite Rule.

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


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

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

If p1 and p2 have the same leading clock, then it is the leading clock
of "p1 or p2".  Otherwise the leading clock of "p1 or 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.]