Property Specification Language: Difference between revisions

Revision as of 10:03, 4 August 2015

Revision as of 12:47, 4 August 2015

Line 1:

'''Property Specification Language''' ('''PSL''') is a languagetemporal developedlogic byextending [[AccelleraLinear temporal logic]] with a range of operators for specifyingboth [[Propertyease (philosophy)|properties]]of orexpression and enhancement of expressive power. PSL makes an extensive use of [[assertionregular (computing)|assertionsexpressions]] aboutand hardwaresyntactic designssugaring. TheIt propertiesis canwidely thenused bein [[functionalthe verification|functionallyhardware verified]]design viaand [[logicverification simulation]]industry, orwhere [[formal verification]]. Sincetools September(such 2004 theas [[standardization|standardmodel checking]]ization) onand/or the language has been done in [[IEEElogic simulation]] 1850tools workingare group.used Into Septemberprove 2005,or therefute IEEEthat 1850a Standardgiven forPSL Propertyformula Specificationholds Languageon (PSL)a wasgiven announceddesign.

PSL was initially developed by [[Accellera]] for specifying [[Property (philosophy)|properties]] or [[assertion (computing)|assertions]] about hardware designs. 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.

Property Specification Language is a temporal logic extending [[Linear temporal logic]] 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.

== TechnicalSyntax detailsand Semantics ==

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:

Line 10:

The property "every {{color|orange|request}} which is immediately followed by an {{color|orange|ack}} signal, should be followed by a compete {{color|orange|data transfer}}, where a complete data transfer is a sequence starting with signal {{color|orange|start}}, ending with signal {{color|orange|end}} in which {{color|orange|busy}} holds at the meantime can be expressed by the PSL formula:

<source> ((true[*]; req; ack) |=> (start; busy[*]; end) </source>

A trace satisfying this formula is given in the figure on the right.

[[File:The trigger operator - slide 1.jpg|thumb|a simple trace satisfying <source>(true[*]; req; ack) |=> (start; busy[*]; end)</source>]]

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

===Operators===

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

==== SERE-style Operators====

The most commonly used PSL operator is the "suffix-implication" operator (a.k.a the "triggers" operator), which is denoted by {{code|{{!}}=<math> \mapsto </math>}}. Its left operand is a PSL regular expression and its right operand is any PSL formula (be it in LTL style or regular expression style). The semantics of {{code|r{{!}}=<math>r \mapsto p}}</math> is that on every time point i such that the sequence of time points up to i constitute a match to the regular expression r, the path from i+1 should satisfy the property p. There is also a non-overlapping version, which requires p to hold from time i+1 rather than i. This is exemplified in the picturesfigures on the right.

[[File:The trigger operator - slide 2.jpg|thumb|path satisfying ''r triggers p'' in two non-overlapping ways]]

[[File:The trigger operator - slide 3.jpg|thumb|path satisfying ''r triggers p'' in two overlapping ways]]

[[File:The trigger operator - slide 4.jpg|thumb|path satisfying ''r triggers p' in three ways]]

The regular expressions of PSL have the common operators for concatenation ({{color|red|;}}), Kleene-closure ({{color|red|*}}), and union ({{color|red|{{code|{{!}}}}}}), as well as operator for fusion ({{color|red|:}}), intersection ({{color|red|&&}}) and a weaker version ({{color|red|&}}), and many variations for consecutive counting {{color|red|[*n]}}, {{color|red|[and in->n]}}consecutive counting, e.g. {{color|red|[=->n]}}.

The trigger operator comes in several variations, shown in the table below.