Property Specification Language Tutorial

Previous: What is an assertion language?| Next: Anatomy of a PSL Assertion (contd.)

Anatomy of a PSL assertion

A quick start example.

Figure 1: Anatomy of a PSL assertion.

Figure 1 shows various pieces that comprise a complete PSL assertion. The next sections delve into individual pieces.


PSL allows optional label to be specified for every assertion. It is a recommended practice to use a meaningful name to each assertion. It helps in identifying any failures, success reports coming from a PSL aware tool.

Verification directive

PSL provides a rich set of constructs to build complex properties. A property by definition is a declaration and a verification tool doesn’t know what to do with it unless told otherwise. A Verification directive sits on top of a property and instructs a tool (simulator or a model checker) whether to "check" that the property is never violated, or "look for occurrence of the property" etc.

When to check?

As part of the temporal layer, PSL provides means to specify "when to check for a property". Loosely speaking they can also be called as 'occurrence operators'. PSL supports the following occurrence operators:

  • always
  • never
  • eventually!
  • next (family of them).
The always operator is the most frequently used one and it specifies that the following property expression should be checked every clock.

Previous: What is an assertion language? | Next: Anatomy of a PSL Assertion (contd.)


Verification Management
Join Verification Management Group

Shop Amazon - Contract Cell Phones & Service Plans

Book of the Month