Property Specification Language: Difference between revisions

Revision as of 17:31, 3 August 2015

Revision as of 04:32, 4 August 2015

Line 1:

''Property Specification Language (PSL)'', is a temporal logic extending [[Linear temporal logic|(LTL)]] with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of [[regular expressions]] and syntactic sugaring. It is widely used in the hardware design and verification industry, where [[formal verification]] tools (such as [[model checking]]) are used to prove or refute that a given PSL formula holds on a given design.

==== Examples ====

PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a {{color|orange|request}} should always eventually be {{color|orange|grant}} ed can be expressed by the PSL formula:

<source> always (request -> eventually! grant)