Property Specification Language (PSL)

PSL is a linear-time temporal algebra designed for RTL engineering. The PSL language is now part of the System Verilog assertion language.

»www.project-veripage.com/psl_tutorial_2.php

General structure of a PSL assertion

1. always and never,
2. next,
3. eventually!

The always directive is the most frequently used and it specifies that the following property expression should be checked every clock. The never directive is a shorthand for a negated always.

The next directive relates successive state properties, as qualified by the clocking event and qualifying guard.

The eventually! directive is for liveness properties that relate to the future. The eventually! directive is suffixed with a bang sign to indicate it is strong property that cannot be (fully) checked with simulation.

For hands-on experience, see a previous ACS exercise: »Dynamic validation using Monitors/Checkers and PSL