DRAFT, 2-NOV-2003

SVA 3.1A PROPOSAL:  INSTANTIATION OF PROPERTIES
-----------------------------------------------

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

This proposal extends the SVA language by allowing instances of
defined properties to serve as property expressions.

Users need to be able to decompose complicated properties into simpler
pieces is essential.  In SVA 3.1, the property forms are so limited
that instantiation of named sequences is adequate to achieve
decomposition.

The current proposal is needed if any of the proposals on generalized
implications or boolean property operators is passed.

EXAMPLE:  If the generalized implication proposal passes, then the user will 
be able to define

   property p1;
      s1 |=> (s2 |=> s3);
   endproperty

If the subproperty "s2 |=> s3" is shared with other properties or 
is useful to compartmentalize, the user may want to define

   property p0;
      s2 |=> s3;
   endproperty

   property p1;
      s1 |=> p0;
   endproperty

////

This proposal is in alignment with proposed Accellera PSL 1.1.


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:
-----------------------------------------

None.  The formal semantics does not deal with instantiation.