Property Specification Language Tutorial
Previous: Property Expression: Temporal layer |
Next: Verification and Modeling Layers
Property Expressions: Temporal Layer (contd.)
Properties
In PSL, a Property forms the top level place holder for the expected design behavior. A property
can instantiate named sequences, boolean expressions and other sub-ordinate properties and
combine them using various property operators described in the following sections.
Suffix Implication operators
Many a class of design properties exhibit a 'cause-and-effect' phenomenon, i.e. a property/sequence
(condition-to-be-checked, or effect) is expected to hold only after a triggering-condition (or cause)
occurs. This is also referred to as an implication operator. PSL provides two variants of implication
operators that are described in the following sub-sections. A procedural way of understanding these
implication operators is to visualize them as:
if (triggering-condition)
condition-to-be-checked
Now, in a typical if construct, an else part is provided and is an interesting branch to verify as well, but
in PSL, the else part is treated as Vacuous success - meaning that if the triggering-condition doesn’t
hold, don’t bother to check any thing and return a TRUE. But this is not a real success and is treated
as vacuous success.
A. Overlapping suffix implication (|->) operators
The condition-to-be-checked is checked in the same clock as the triggering-condition
occurs. For example, to describe a property as: 'Whenever there is a new packet (indicated by
packet_start), the pkt_xfer_en_n should be low'.
pkt_start |-> !pkt_xfer_en_n
B. Non-overlapping suffix implication (|=>) operator
This is a variant of the previous overlapping operator, and with this, the condition-to-be-checked
is checked ONE CLOCK after the triggering-condition occurs. A simple example would be to check for
a FIFO full:
fifo_almost_full |=> fifo_push |-> fifo_full;
The above property described that once the fifo is almost full, a push in the next clock cycle shall make
the fifo_full to be asserted (in the same clock as the fifo_push occurred).
Occurrence operators
As mentioned in the introduction section, PSL provides few operators to specify when to check for the
property, in LRM they are referred to as 'simple FL properties' and in this tutorial they are termed
as 'occurrence operators' solely for the purpose of descriptiveness. PSL supports always, never,
eventually!, next operators.
- always operator specifies that the property should hold in every cycle.
- never operator specifies that the following property should not hold during any cycle.
- eventually! operator requires that the property shall hold in some cycle in the future but before
the end of verification process.
- next is a family of operators, basically expressing a requirement that the property following this
operator shall hold in the next cycle(s).
until operator
An until operator requires that first property hold till the second property holds. e.g.
pkt_sop |-> !pkt_xfer_en_n until pkt_eop
The above property describes that once, a packet is started, the xfer_en_n shall be low until the packet
ends.
before operator
A before operator requires that the one property hold before another. In a typical processor environment,
an opcode_fetch process should occur before an execute_opcode phase, the following PSL property captures
that requirement.
opcode_fetch before execute_opcode;
abort operator
In almost any practical property, there is a need to abort the checking in case of a reset, soft reset,
pkt_abort etc. abort operator is intended to capture that intent. Using one of the previous packet
transaction examples,
({pkt_sop} |-> {!pkt_xfer_en_n until pkt_eop}) abort pkt_abort;
The above property aborts checking once a pkt_abort is seen.
Previous: Property Expression: Temporal layer |
Next: Verification and Modeling Layers
|