Property Specification Language
Property Specification Language (PSL) is a temporal logic extending linear temporal logic with a range of operators for both ease of expression and enhancement of expressive power.
It is widely used in the hardware design and verification industry, where formal verification tools (such as model checking) and/or logic simulation tools are used to prove or refute that a given PSL formula holds on a given design.
PSL was initially developed by Accellera for specifying properties or assertions about hardware designs.
In September 2005, the IEEE 1850 Standard for Property Specification Language (PSL) was announced.
For instance, the property "a request should always eventually be granted" can be expressed by the PSL formula: The property "every request that is immediately followed by an ack signal, should be followed by a complete data transfer, where a complete data transfer is a sequence starting with signal start, ending with signal end in which busy holds at the meantime" can be expressed by the PSL formula: A trace satisfying this formula is given in the figure on the right.
The regular expressions of PSL have the common operators for concatenation (;), Kleene-closure (*), and union (|), as well as operator for fusion (:), intersection (&&) and a weaker version (&), and many variations for consecutive counting [*n] and in-consecutive counting e.g. [=n] and [->n].
Operators for concatenation, fusion, union, intersection and their variations are shown in the table below.
Truncated paths occur in bounded-model checking, due to resets and in many other scenarios.
PSL subsumes the temporal logic LTL and extends its expressive power to that of the omega-regular languages.
(true[*]; req; ack) |=> (start; busy[*]; end)
