PSL is a property specification language. It is a means to express properties of a design, and in addition to specify how verification tools should use those properties. For example, a property may be asserted his specifies that the design in question is expected to behave as described by the property. A property may also be assumed his specifies that the design in question expects its inputs to behave as described by the property. PSL also provides other directives, for instance a means to specify scenarios that should be covered.

PSL is much more than simply an assertion language. Nevertheless, assertions are at the heart of PSL, and many PSL users will use PSL only for its assertion capabilities. Thus, before we examine the complete language, a few words about what exactly a PSL assertion is are in order. Many programming languages (for example Java) and hardware description languages (for example VHDL) contain assert constructs. An assert construct provides the user with a way to check at run time or at simulation time that a certain condition holds, and to report a warning or an error if it does not. PSL assertions are similar in motivation, but much more extensive in their scope. In addition to simple Boolean conditions, a PSL assertion can contain temporal operators that allow the user to describe relations over time. For example, the PSL assertion assert always (a -> next b); specifies that whenever signal a holds, signal b