Property Specification Language: Difference between revisions

Revision as of 15:09, 3 August 2015

Revision as of 15:34, 3 August 2015

Line 1:

'''Property Specification Language''' ('''PSL''') is a language developed by [[Accellera]] for specifying [[Property (philosophy)|properties]] or [[assertion (computing)|assertions]] about hardware designs. The properties can then be [[functional verification|functionally verified]] via [[logic simulation]] or [[formal verification]]. Since September 2004 the [[standardization|standard]]ization on the language has been done in [[IEEE]] 1850 working group. In September 2005, the IEEE 1850 Standard for Property Specification Language (PSL) was announced.

==Technical specifications==

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)

Line 12:

===Operators===

PSL's temporal operators can be roughly classified into LTL-style operators and regular-expression-style operators. Many PSL operators come intoin two versions, a strong version, indicated by an exclamation mark suffix ( {{color|red|!}} ), and a weak version. The ''strong versionsversion'' makemakes eventuality requirements (i.e. require that something will hold in the future), while the ''weak version'' dodoes not. An ''underscore suffix'' ( {{color|red|_}} ) is used to differentiate "''inclusive"'' vs. "''non-inclusive"'' requirements. An {{color|red|a_}} and {{color|red|e_}} suffixes aare used to denote ''universal'' vs. ''existential'' requirements. Exact time windows are denoted by {{color|red|[n]}} and flexible by {{color|red|[m..n]}}.

==== LTL-style Operators====

Below is a sample of some LTL-style operators of PSL:.

Here {{color|orange|p}} and {{color|orange|q}} are any PSL formulas.

{| class="wikitable"