API and Attributes for PSL

Proposal Editing Information

• Who Updates: JimLewis, <Add YourName >, ...
• Date Proposed: 2012-08-17
• Date Last Updated: 2016-Dec-27
• Priority:
• Complexity:
• Focus: Testbench
• Proposal Maturity: Finalizing for LCS

Requirement Summary

Make PSL more usable in VHDL. Currently PSL constructs have full access to VHDL objects, but VHDL code cannot manipulate or interrogate PSL constructs. We propose reading PSL temporal constructs in VHDL and adding attributes to PSL assert and cover directives. We may want to add these attributes to properties and sequences as well.

Minimally when a test finishes, it needs to check:

• Did any assert fail?
• Did all covers trigger at least once?
• When validating that asserts work, did all assert directives trigger at least once?

Rationale

Currently there are is no feedback from assertions to VHDL code so that a testbench can react to an assertion. Also, from a designer perspective, PSL temporal constructs are very powerful for expressing sequences. This can be leveraged in synthesizable code e.g. to check assumptions and detect problems.

Related and/or Competing Issues:

Related proposal: VHDL Assert API

Proposal

Basic PSL Attributes

The static name of a PSL directive (assert, cover, ...) is the statement label of the corresponding directive. If a PSL directive does not have a statement label, it does not have a static name.

Is there any reason to try to reason about a PSL sequence or property? It seems that without a directive (assert or cover), a simulator has no reason to be tracking information about a particular sequence or property. The static name for these could be defined as follows:

The static name of a PSL property or sequence that does not have parameters is the name of the property or sequence. If the PSL property or sequence has parameters, it does not have a static name.

P'SIGNAL

Kind: Signal.
Prefix: Any PSL directive (assert, cover, ...) 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).  A PSL assert 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.

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.

Intent: Allow a process which is triggered off of multiple different events to determine if a particular PSL object changed during the execution. P'EVENT is an abbreviation for P'SIGNAL'EVENT.

Extended PSL Attributes

P'TRANSACTION

Kind: Signal.
Prefix: Any sequence, property, assert, or cover denoted by the static name P.
Result type: Type BIT. 
Result: A signal whose value toggles to the inverse of its previous value in each 
simulation cycle in which sequence, property, assert, cover completes. 
Restrictions: A description is erroneous if it depends on the initial value of P'TRANSACTION. 

Intent: Trigger a process on completion of a PSL sequence, propoerty, assert, or cover

P'COUNT

Allows a count of specific cover (and assert) directives to be accessed. Really intended to detect which

duplicates GetPslCount. Do we need this? If we decide against VHDL_Assert_Label'count, then this should be deleted.

Kind: Function.
Prefix: Any defined assert, cover denoted by the static name P.
Result type: Type INTEGER.
Result: The number of times an assert or cover statement has completed.

Basic API - Defined in std.env

PSL Assert Failed

impure function PslAssertFailed return boolean ; 

Returns TRUE if any PSL assert statement triggered during a simulation.

Clear VHDL Assert Errors

procedure ClearVhdlAssert return boolean ; 

Clears any sense of VHDL Assert having been executed. After calling ClearVhdlAssert, VhdlAssertFailed will return FALSE. Allows a VHDL testbench to clear alerts after reset or between tests.

PSL Is Covered

impure function PslIsCovered return boolean; 

Returns TRUE if all PSL covers are covered.

Psl Cover Asserts

procedure SetPslCoverAssert( Enable : boolean := TRUE) ; 
impure function GetPslCoverAssert return boolean ; 

When Enable is TRUE, a PSL assert directive shall define both an assert and a cover. When Enable is FALSE, PSL asserts only define an assert.

Psl Is AssertCovered

impure function PslIsAssertCovered return boolean ; 

Returns TRUE if GetPslIsAssertCovered is true and all asserts are covered.

Intent: allows a test to validate that improper behavior can trigger an assert.

Extended API - Defined in std.env

PSL Assert Count

impure function GetPslAssertCount return integer ; 

Returns the number of times PSL assert statements have triggered during a simulation. Generally a count of 1 indicates a test has failed.

Psl Enable, Disable

procedure SetPslEnable(psl psl_name ; Enable : boolean := TRUE) ; 
impure function GetPslEnable(psl psl_name) return boolean ; 

When Enable is TRUE, enable the corresponding severity level. When Enable is FALSE, disable the corresponding severity level.

Advanced API

PSL Goal

procedure SetPslGoal(psl psl_name ; Count : integer := integer'right) ; 
impure function GetPslGoal(psl psl_name ) return integer ; 

Sets the number of cover (or assert) that must happen before coverage is considered covered. For cover objects, the count defaults to 1. For assert objects, the count defaults to 0.

Note on the simulation run in which assertions are validated, it is desirable to set these to 1 for assert objects to verify that each has indeed been triggered.

PSL Stop Count

procedure SetPslStopCount(psl psl_name ; Count : integer := integer'right) ; 
impure function GetPslStopCount(psl psl_name ) return integer ; 

Count sets the number of the corresponding assert or covers that can happen before the simulation stops. For cover objects, the count defaults to integer'right. For assert objects, the count defaults to ?integer'right? (alternative is to set it to 0 which is stop if any occur).

PSL Count

impure function GetPslCount(psl psl_name ) return integer ; 

Returns the number of times a named cover or asset has triggered.

Advanced API - Defined in std.env

These features is where OSVVM's coverage package started with Intelligent Coverage. If one can get the hole count, randomly pick a value between 1 and the hole count, then get information about the object (in this case its name), one can write a program that does a random walk across the coverage model.

Perhaps we need to consider specifying a data structure for some of the features that are recorded in the basic section (such as SetPslGoal)

GetPslHoleCount

impure function GetPslHoleCount return integer ; 

Returns the sum of the values of maximum(0, GetPslGoal - GetPslCount) across all PSL objects (cover and asserts)

GetPslHoleName

impure function GetPslHoleName(index : integer := 1) return string; 

Returns the name of a PSL object as a string that corresponds to the N'th PSL hole.

Intent: Using this, a testbench can iteratively or randomly select the one of the uncovered items and use its name to cause the testbench to change its settings/controls with the intent of working toward covering the item.

Reading PSL properties

The following is a slightly modified version of the example from Ashenden's book, "The Designer's Guide to VHDL", third edition, section 18.3, page 577.

library ieee;
context ieee.ieee_std_context;

entity slave is
  port ( clk, reset : in  std_ulogic;
         req        : in  std_ulogic;
         ack        : out std_ulogic;
         lost_ack   : out std_ulogic; -- this is new
         ...);
end entity slave;

architecture pipelined of slave is
  signal req_cnt, ack_cnt : unsigned(3 downto 0);
  
  default clock is rising_edge(clk);
  property all_requests_acked is
    forall C in {0 to 15}:
      always {req and req_cnt = C} |=>
             {[*0 to 99]; ack and ack_cnt = C};
  
begin
  req_ack_counter: process (clk) is
  begin
    if clk'event and clk = '1' then
      if reset = '1' then
        req_cnt <= "0000";
        ack_cnt <= "0000";
        lost_ack <= '0';
      else
        if req = '1' then req_cnt <= req_cnt + 1; end if;
        if ack = '1' then ack_cnt <= ack_cnt + 1; end if;

        -- new stuff here
        if not all_requests_acked then
          lost_ack <= '1';
        end if;
        -- end new stuff
      end if;
    end if;
  end process req_ack_counter;

  assert all_requests_acked;
  
end architecture pipelined;

Each PSL sequence (or any temporal construct) is a boolean valued expression that is FALSE if it is violated by the sequence of events terminating at the current instant.

There is no reason for a simulator to be tracking a sequence or property that is not in a directive (such as assert or cover).

Questions

General Comments

-- TorstenMeissner - 2016-08-08: I support this proposal, as I use PSL for assertions & functional coverage very often. At the moment, the only way to get informations from the PSL side, is to use the PSL ended() function or the deprecated PSL endpoint construct. In Mentor Tools (Modelsim & Questa) the state of these two constructs are readable in the VHDL code which has the same context as the PSL code. I don't know, if this feature is defined in the PSL standard, or if it is a Mentor enhancement. Tristan has also implemented the reading of PSL endpoint state from VHDL some time ago. I don't know if other simulators support this. So it would be good to have a way get informations about PSL directives in VHDL code, which is standardized in a future VHDL version. Hopefully that feature would be implemented by all VHDL standard conform simulators.

Supporters

-- TorstenMeissner - 2016-08-08 -- RyanHinton - 2016-12-28

Add your signature here to indicate your support for the proposal