Property Specification Language: Difference between revisions

Revision as of 23:15, 21 December 2022

Revision as of 19:03, 27 December 2022

Line 5:

== Syntax and semantics ==

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

<syntaxhighlight lang="text"> always (request -> eventually! grant)

</syntaxhighlight>

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

<syntaxhighlight lang="text"> (true[*]; req; ack) |=> (start; busy[*]; end) </syntaxhighlight>

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 <syntaxhighlight lang="text">(true[*]; req; ack) |=> (start; busy[*]; end)</syntaxhighlight>]]

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 ( {{mono|!}} ), 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'' ( {{mono|_}} ) is used to differentiate ''inclusive'' vs. ''non-inclusive'' requirements. AnThe {{mono|_a}} and {{mono|_e}} suffixes are used to denote ''universal'' (all) vs. ''existential'' (exists) requirements. Exact time windows are denoted by {{mono|[n]}} and flexible by {{mono|[m..n]}}.

=== SERE-style operators===

The most commonly used PSL operator is the "suffix-implication" operator (a.k.a.also known as the "triggers" operator), which is denoted by {{mono|{{!}}{{=}}>}}. 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 {{mono|r {{!}}{{=}}> p}} 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. This is exemplified in the figures 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 ({{mono|;}}), Kleene-closure ({{mono|*}}), and union ({{mono|{{!}}}}), as well as operator for fusion ({{mono|:}}), intersection ({{mono|\&\&}}) and a weaker version ({{mono|\&}}), and many variations for consecutive counting {{mono|[*n]}} and in-consecutive counting e.g. {{mono|[{{=}}n]}} and {{mono|[->n]}}.

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

Line 71:

|-

| <code> s within t </code>

| match of s within a match of t, abbreviation of ([*]; s; [*]) && (t)

|-

|}

Line 197:

=== Sampling operator===

Sometimes it is desirable to change the definition of the ''next time-point'', for instance in multiply-clocked designs, or when a higher level of abstraction is desired. The ''sampling operator'' (a.k.a.also known as ''the ''clock operator''), denoted {{mono|@}}, is used for this purpose. The formula {{mono| p @ c }} where {{mono| p}} is a PSL formula and {{mono|c}} a PSL Boolean expressions holds on a given path if {{mono| p}} on that path projected on the cycles in which {{mono| c}} holds, as exemplified in the figures to the right.

[[File:Need for multiple clocks.jpg|thumb|path and formula showing need for a sampling operator]]

The first property states that "every {{mono|request}} whichthat is immediately followed by an {{mono|ack}} signal, should be followed by a complete {{mono|data transfer}}, where a complete data transfer is a sequence starting with signal {{mono|start}}, ending with signal {{mono|end}} in which {{mono|data}} should hold at least 8 times:

<syntaxhighlight lang="text"> (true[*]; req; ack) |=> (start; data[=8]; end) </syntaxhighlight>

But sometimes it is desired to consider only the cases where the above signals occur on a cycle where {{mono|clk}} is high.

Line 232:

===Expressive power===

PSL subsumes the temporal logic [[Linear temporal logic|LTL]] and extends its expressive power to that of the [[omega-regular languages]]. The augmentation in expressive power, compared to that of LTL, which has the expressive power of the star-free ω-regular expressions, can be attributed to the ''suffix implication'', a.k.a.also known as the ''triggers'' operator, denoted "|->". The formula ''r |-> f'' where ''r'' is a regular expression and ''f'' is a temporal logic formula holds on a computation ''w'' if any prefix of ''w'' matching ''r'' has a continuation satisfying ''f''. Other non-LTL operators of PSL are the ''@'' operator, for specifying multiply-clocked designs, the ''abort'' operators, for dealing with hardware resets, and ''local variables'' for succinctness.

===Layers===

Line 254:

*{{Cite book| title = 1850-2010 – IEEE Standard for Property Specification Language (PSL)| doi = 10.1109/IEEESTD.2010.5446004| year = 2010| isbn = 978-0-7381-6255-3}}

**IEC 62531:2012 {{Cite book| title = 62531-2012 – IEC 62531:2012(E) (IEEE Std 1850-2010): Standard for Property Specification Language (PSL)| doi = 10.1109/IEEESTD.2012.6228486| year = 2012| isbn = 978-0-7381-7299-6}}

*{{cite book|doi=10.1007/978-3-540-45069-6_3|chapter=Reasoning with Temporal Logic on Truncated Paths|title=[[Computer Aided Verification]]|volume=2725|pages=27|series=Lecture Notes in Computer Science|year=2003|last1=Eisner|first1=Cindy|last2=Fisman|first2=Dana|last3=Havlicek|first3=John|last4=Lustig|first4=Yoad|last5=McIsaac|first5=Anthony|last6=Van Campenhout|first6=David|isbn=978-3-540-40524-5|chapter-url=http://www.research.ibm.com/people/e/eisner/papers/cav49.pdf}}

*{{cite book|doi=10.1007/3-540-45061-0_67|chapter=The Definition of a Temporal Clock Operator|title=Automata, Languages and Programming|volume=2719|pages=857|series=Lecture Notes in Computer Science|year=2003|last1=Eisner|first1=Cindy|last2=Fisman|first2=Dana|last3=Havlicek|first3=John|last4=McIsaac|first4=Anthony|last5=Van Campenhout|first5=David|isbn=978-3-540-40493-4|chapter-url=http://www.cis.upenn.edu/~fisman/documents/EFHMV_ICALP03_full.pdf}}