Attributes for PSL

Proposal Editing Information

• Who Updates: JimLewis, <Add YourName >, ...
• Date Proposed: 2012-08-17
• Date Last Updated: 2012-08-17
• Priority:
• Complexity:
• Focus: Testbench
• Proposal Maturity: Brainstorming

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.

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: VHDL ASSERT API

Proposal

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;

The basic idea is to be able to use a PSL sequence (or any temporal construct) as a boolean expression that is false if it is violated by the sequence of events terminating at the current instant. (Is this what I'm really trying to say?)

PSL Attributes

Need to correlate these with SystemVerilog capability.

P'TRANSACTION

The intent is to be able to trigger a process on completion of a PSL sequence, property, assert, or cover

Kind: Signal.
Prefix: Any defined 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. 

P'EVENT

If multiple different properties can trigger a process, this one allows us to detect which one triggered the process

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.

P'COUNT

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

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.

PSL API - Predefined Functions

type HIER_LEVEL_TYPE is (CURRENT, BELOW) ;

HIER parameter specifies if the command applies the the current level of hierarchy or current level plus below.

These names could be better, any suggestions?

PATH parameter specifies the path in a consistent manner with external name specifications.

PSL_ENABLE

procedure PSL_ENABLE(PATH : STRING := "."; HIER : HIER_LEVEL_TYPE := CURRENT) ;

Enables PSL directives on path.

Intent: Turn on PSL assertions after reset

PSL_DISABLE

procedure PSL_DISABLE(PATH : STRING := "."; HIER : HIER_LEVEL_TYPE := CURRENT) ;

Disables PSL directives within the scope of path.

Intent: Turn off PSL assertions during reset. Turn off PSL assertions not for this test

PSL_COUNT_COVER

function PSL_COUNT_COVER(AtLeast : integer := 1 ; PATH : STRING := ".") return natural;

Returns the number of cover directives whose count is less than the AtLeast parameter.

Intent: When Coupled with PSL_GET_COVER_NAME enables access to all items that are not covered yet. Using this, a testbench can iteratively or randomly select the one of the uncovered bins and use its name to cause the testbench to change its settings/controls with the intent of working toward covering the item.

PSL_GET_COVER_NAME

function PSL_GET_COVER_NAME(AtLeast : integer := 1 ; N : INTEGER := 1 ; PATH : STRING := ".") return string;

Returns the string value of the name of the N'th PSL cover object whose a count less than the AtLeast parameter. The PATH parameter specifies the path of the design

Intent: When Coupled with PSL_COUNT_COVER enables access to all items that are not covered yet. Using this, a testbench can iteratively or randomly select the one of the uncovered bins and use its name to cause the testbench to change its settings/controls with the intent of working toward covering the item.

PSL_COUNT_ASSERT

function PSL_COUNT_ASSERT(PATH : STRING := ".") return natural;

Returns the number of assert directives whose count is greater than 0.

Intent: When Coupled with PSL_GET_ASSERT_NAME access identification of all assertions that have triggered during this simulation.

PSL_GET_ASSERT_NAME

function PSL_GET_ASSERT_NAME(N : INTEGER := 1 ; PATH : STRING := ".") return natural;

Returns the string value of the name of the N'th PSL assert object whose a count greater than the 0. The PATH parameter specifies the path of the design.

Intent: When Coupled with PSL_COUNT_ASSERT enables identification of all assertions that have triggered during this simulation.

Use Models

Questions

Enable/Disable functionality - one procedure with parameters or two procedures

Enable/Disable functionality - how to handle hierarchy below the current level?

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

Add your signature here to indicate your support for the proposal