TWiki
>
P1076/Ballots Web
>
Vhdl2019CollectedRequirements
>
PslAttributes
(2020-02-17,
JimLewis
)
(raw view)
E
dit
A
ttach
---+ Attributes for PSL <br />%TOC% ---++ Proposal Editing Information * Who Updates: Main.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. <pre>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; </pre> 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 <pre>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. </pre> ---++++ P'EVENT If multiple different properties can trigger a process, this one allows us to detect which one triggered the process <pre>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. </pre> ---++++ P'COUNT Allows a count of specific cover (and assert) directives to be accessed. Really intended to detect which <pre>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. </pre> ---+++ 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 -- Main.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 -- Main.TorstenMeissner - 2016-08-08 _Add your signature here to indicate your support for the proposal_
E
dit
|
A
ttach
|
P
rint version
|
H
istory
: r6
<
r5
<
r4
<
r3
<
r2
|
B
acklinks
|
V
iew topic
|
Ra
w
edit
|
M
ore topic actions
Topic revision: r6 - 2020-02-17 - 15:34:57 -
JimLewis
P1076/Ballots
Log In
or
Register
P1076/Ballots Web
Create New Topic
Index
Search
Changes
Notifications
RSS Feed
Statistics
Preferences
Webs
Main
P1076
Ballots
LCS2016_080
P10761
P1647
P16661
P1685
P1734
P1735
P1778
P1800
P1801
Sandbox
TWiki
VIP
VerilogAMS
Copyright © 2008-2024 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki?
Send feedback