PSL Use Models

The following is for discussion in the next Issues SC meeting.

PSL Use Models
=============

Following is a summary of a number of PSL use models and variations that might be 
worth addressing in the 1850 LRM.  The names I've used below are somewhat arbitrary; 
they are intended only to help differentiate the various cases, and should not be viewed 
as standard names.  I've described each use model to the best of my ability, but it is 
quite possible that some of the descriptions would benefit from some tweaking (i.e., 
small changes might make the description apply to a larger, but still distinct, usage 
category).  

1a. Abstract Use Model.

This use model involves using PSL to model behavior requirements, independent of 
any design.  In this case, the requirements are expressed in terms of variables defined 
in PSL vunits.  In this use model, formal verification can be used to reason about the 
abstract requirements - e.g., to check for vacuity, to check that dual sets of requirements 
(e.g., master/slave requirements) are complementary, or to check that cover directives 
and a set of assumptions are consistent (e.g., all cover directives are reachable in the 
context of the assumptions).  This use model may be less appropriate for simulation, 
unless the vunits contain enough auxiliary code to define a simulatable model - in 
which case, the usage probably fits into one of the other cases.

1b. Concrete Use Model.

This use model involves using PSL to model behavior requirements for a particular 
design.  In this case, the requirements are expressed in terms of variables defined in 
the HDL design, possibly augmented with auxiliary code (and associated variables) 
defined in PSL vunits.  In this use model, formal verification can be used to verify 
that the design behavior is consistent with the requirements expressed in PSL.  
Simulation can also be used to test whether a particular input sequence will cause the 
design to behave in a manner that conflicts with the requirements.

2a.  Focused Use Model.

This approach involves defining PSL vunits specifically to verify a particular behavior.  
For example, one might write a vunit for each verification task.  In the limit, each vunit 
would contain (or inherit) one assertion to verify.   Each vunit would also contain (or 
inherit) a set of assumptions and optionally auxiliary code that define the environment 
in which the assertion should be verified.  The assertion, assumptions, and auxiliary 
code can be abstract (see 1a) or can refer to objects within an HDL design (see 1b).  

In the latter case, vunits tend to be bound to particular instances of HDL modules, and 
it may be appropriate for them to inherit vunits that are bound to other HDL module 
instances.  Instance binding is appropriate here because each verification run targets a 
particular behavior of the design, and therefore a particular portion of the elaborated 
design hierarchy.  Module binding would typically be used only when binding to the 
root module of the whole design.

This use model emphasizes the role of a vunit in defining the verification task at hand.  
It is appropriate for formal verification.

2b.  Distributed Use Model.

This approach involves associating assertions with HDL design modules by placing 
them in vunits that are each bound to one of the modules.  In this use model, PSL 
directives are used to specify behavioral requirements for the module, so that those 
requirements are carried along to any design in which the module is used.  For 
example, the input requirements for a module could be expressed as assumptions; the 
internal computation requirements and output requirements of the module could be 
expressed as assertions.  In this use model, directives act more as behavioral 
specifications, and less as tool directives.  The use model is distributed in the sense 
that the assertions to be verified are distributed throughout the design, and all 
requirements are presented at the same time, rather than focusing on one requirement 
at a time.  

In this use model, vunits tend to inherit only unbound vunits used to define shared 
resources.  (Note that in the general case, we can't assume any particular relationship 
will apply between two modules A and B (as opposed to particular instances of those 
modules), except when one instantiates the other.  As a result, it doesn't make sense 
for a vunit bound to A to inherit a vunit bound to B, unless module A instantiates 
module B.)

This use model emphasizes the role of a vunit as  means of collecting up all behavioral 
requirements associated with a design module, independent of the verification method.  
It is particularly appropriate for simulation, but can be used for formal verification also.  

There are also variations on the above use models.  These include the following:

3. vmode/vprop Use Model.

This is a variation in which assertions and assumptions are segregated into different 
vunits.  This approach provides some structure to help ensure reuse of assumptions.  
For example, in the Focused Use Model, one might create a vmode for each module 
or instance in the design, containing a set of assumptions about the behavior of that 
module or instance.  Then a vprop could be created, containing a particular assertion 
to verify, and both the vprop and the vmodes necessary to verify it could be inherited 
into a common vunit.  The vmodes could also be inherited into other vunits to verify 
assertions written in other vprops.

4. Flexible Use Model.

This is a variation in which all design behavior is described using assertions.  This 
approach avoids the need to create both assertions and assumptions about the same 
behavior, and instead allows the user or the tool to decide that, for a given verification 
task, certain assertions should be converted to assumptions, or vice versa.  For example, 
in the Distributed Use Model, if simulation is used, this approach allows the simulator 
to convert assumptions to assertions, so that all behavior specifications are checked 
during simulation, even those that were defined as assumptions.  Similarly, if formal 
verification is used, this approach allows the tool to convert assertions about the 
top-level inputs (which cannot be verified in this run) to assumptions that can be used 
to constrain the verification run, with the understanding that they must still be verified 
at the next higher level of integration.

5. Assert-Only Use Model.

The Flexible Use Model can be taken one step further, so that the user only writes 
assertions, and never writes assumptions.  In this use model, no extra work is involved 
for simulation, since all behavioral specifications are already expressed as assertions.  
For formal verification, the user and/or the tool must determine which assertions to 
use as assumptions for verifying any given assertion or collection of assertions.  The 
natural choice is to use assertions about the inputs of a design, i.e., those that depend 
upon at least one input signal to pass non-vacuously, as constraints under which the 
other assertions are to be verified.  This approach is particularly appropriate when 
assertions are embedded in design code rather than written in separate vunits.  (See 6.)

6.  Embedded Use Model.

This is a variation of the Distributed Use Model in which PSL directives are embedded 
in HDL source code, using the comment convention that most (all?) EDA vendors support.  
This usually involves assertions only, as in the Assert-Only Use Model, except that if OVL 
modules are used to embed assertions in the design, the underlying OVL implementation 
contains either assertions or assumptions, depending upon the setting of a generic 
parameter in the OVL instantiation.

Some other variations that might be worth identifying:

 - binding to the top-level module only, and using hierarchical pathnames to refer to 
specific instances of design objects; vs. binding to each module in the design hierarchy, 
and using simple names to refer to design object definitions.

 - compilation of PSL to checkers that are linked with a compiled design later, vs. 
compilation of PSL at the same time the design is compiled

 - use of PSL to express properties/assertions that are checked against simulation traces 
rather than checked against the run-time state of a simulation

 - use of PSL vunits to override portions of the functionality of the design to which they 
are bound




-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.