Language Change Specification for API and Attributes for PSL

LCS Number:	LCS-2016-043
Version:	2 {16-Jan-2017}
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

Voting Results: Cast your votes here

Yes:

1. Jim Lewis - 2017-01-16 ver 2
2. Patrick Lehmann - 2016-12-31 - ver 1
3. Torsten Meissner - 2017-01-01 - ver 2
4. Peter Flake - 2017-03-09 - ver 2

No:

Abstain:

1. Martin Zabel - 2017-01-23 Any version - I have no experience with PSL.
2. Lieven Lemiengre - 2017-01-27
3. Hendrik Eeckhaut - 2017-01-27 ver 2
4. Yann Guidon - 2017-02-07
5. Brent Hayhoe - 2017-02-16 Version 2 - Abstain due to lack of personal time for review.
6. Martin Thompson- 2017-02-17 Version 2 - I have never used PSL so far so cannot comment.

Revision Notes

Revision 2:

• To 'Signal attribute adds text about assume and restrict directives.

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.

Comments

The defined attributes would be very helpful. They could be useful in testbenches to control the random test stimuli based on the state of PSL directives. I think the P'event attribute is more useful, because it's a function which can be used more flexible in VHDL code. What does complete mean for an PSL assertion? It has reached the end of the underlying property with fail or good state? So after checking the P'event tribute, I would have to use the P'signal attribute to get the concrete completion state of the assertion, I assume.

-- Torsten Meissner - 2017-01-01

I would add following sentence to the Result section of P'SIGNAL. After "A PSL cover value of TRUE indicates that is was satisfied during a given cycle." : "Assume and restrict directives are treated like assert. Fairness directives are not supported."

-- Torsten Meissner - 2017-01-09

Done in version 2

-- Jim Lewis - 2017-01-16

@TODO 2-Mar meeting Does PSL update on postponed cycles? If yes, need to note this in P'Signal and processes using P'Signal must not trigger any delta cycles

-- Jim Lewis - 2017-03-02