Language Change Specification for API and Attributes for PSL

LCS Number:	LCS-2016-043
Version:	2 {16-Jan-2017} 1 {29-Dec-2016}
Date:	16-Jan-2017
Status:	Voting
Author:	Jim Lewis
Email:	Main.JimLewis
Source Doc:	API and Attributes for PSL
More Doc:	history
Summary:	API and Attributes for PSL

Style Notes

Changes are shown in red font. Deletions are crossed out. Editing notes in green font.

Reviewing Notes

This LCS only intends to implement the basic features of the proposal. If an extended or advanced feature of the proposal is to be implemented, it should be implemented by a separate LCS and voted on separately.

Details of Language Change

Section 16.2 Predefined attributes

043.1: new Section to be added on page 254 before section 16.3

16.2.6 Predefined attributes of PSL objects

The static name of a PSL directive (assert, cover, ...) is the statement label of the corresponding directive.

P'SIGNAL
Kind: Signal.
Prefix: Any defined PSL directive (assert, cover, assume, restrict) denoted by the static name P.
Result type: Type BOOLEAN. 
Result: A boolean value indicating the current completion status of a
PSL directive (assert, cover, assume, restrict).
A PSL assert, assume, or restrict value of FALSE indicates that it has failed during a given cycle. 
A PSL cover value of TRUE indicates that is was satisfied during a given cycle.
Fairness directives are not supported.

P'EVENT
Kind: Function.
Prefix: Any defined sequence, property, assert, cover denoted by the static name P.
Result type: Type BOOLEAN.
Result: A value TRUE during each simulation cycle in which sequence, property, 
assert, cover completes.

Note: If a PSL directive does not have a statement label, it does not have a static name.

Section 16.5 Standard environment package

043.2: Add the following subprograms to std.env on page 275 before "end package"

 
    -- PSL Assert Failed
    impure function PslAssertFailed return boolean ;
    
    -- PSL Is Covered
    impure function PslIsCovered return boolean ;
    
    -- Psl Cover Asserts
    procedure SetPslCoverAssert( Enable : boolean := TRUE) ; 
    impure function GetPslCoverAssert return boolean ;
    
    -- Psl Is AssertCovered
    impure function PslIsAssertCovered return boolean ; 
    
    -- Clear PSL State (Assert and Cover)
    procedure ClearPslState ;

043.3: New paragraphs before Notes on page 275

The function PslAssertFailed returns TRUE if any PSL assert statement triggered during a simulation. Immediately after elaboration of a design, PslAssertFailed returns FALSE.

The function PslIsCovered returns TRUE when all enabled PSL objects have reached their goal, otherwise it returns FALSE. Immediately after elaboration of a design, PslIsCovered returns FALSE.

When the procedure SetPslCoverAssert sets Enable to TRUE, a simulator shall handle all PSL assert directives also as cover directives. When the PslCoverAssert Enable is FALSE, a simulator shall handle all PSL assert directives as only assert directives. The function GetPslCoverAssert returns the current value of the PslCoverAssert enable. Immediately after elaboration of a design, GetPslCoverAssert returns FALSE.

The function PslIsAssertCovered returns TRUE if either all asserts are covered and the PslCoverAssert Enable was set to TRUE during simulation of the design. Immediately after elaboration of a design, PslIsAssertCovered returns FALSE.

The procedure ClearPslState clears all internal PSL state information to their after elaboration values.