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

See combined_lrm_changes_1.txt.


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

See combined_lrm_changes_1.txt.   



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

None.  The formal semantics does not deal with instantiation.
