Property Specification Language Tutorial

Previous: Property Expression: Temporal layer | Next: Verification and Modeling Layers

Property Expressions: Temporal Layer (contd.)


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)
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


Verification Management
Join Verification Management Group

Shop Amazon - Contract Cell Phones & Service Plans

Book of the Month