Property Specification Language: Difference between revisions

Revision as of 08:09, 4 September 2015

Latest revision as of 15:33, 7 August 2025

(31 intermediate revisions by 23 users not shown)

Line 1:

{{Short description|Temporal logic}}

'''Property Specification Language''' ('''PSL''') is a [[temporal logic]] extending [[Linearlinear 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]]) 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 [[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.

== Syntax and Semanticssemantics ==

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

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

</syntaxhighlight>

</source>

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

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

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

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

=== SERE-style Operatorsoperators===

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

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

Here {{color|orangemono|s}} and {{color|orangemono|t}} are PSL-regular expressions, and {{color|orangemono|p}} is a PSL formula.

{| class="wikitable"

| <sourcesyntaxhighlight lang="text"> s |=> t! </sourcesyntaxhighlight>

| if there is a match of s, then there is a match of t on the suffix of the trace,

*t starts the cycle after s ends,

*the match of t must reach to its end

|-

| <sourcesyntaxhighlight lang="text"> s |-> t! </sourcesyntaxhighlight>

| if there is a match of s, then there is a match of t on the suffix of the trace,

*t starts the same cycle that s ends,

*the match of t must reach to its end

|-

| <sourcesyntaxhighlight lang="text"> s |=> t! </sourcesyntaxhighlight>

| if there is a match of s, then there is a match of t on the suffix of the trace,

*t starts the cycle after s ends,

*the match of t may "get stuck" in the middle

|-

| <sourcesyntaxhighlight lang="text"> s |-> t </sourcesyntaxhighlight>

| if there is a match of s, then there is a match of t on the suffix of the trace,

*t starts the same cycle that s ends,

Line 53 ⟶ 54:

Operators for concatenation, fusion, union, intersection and their variations are shown in the table below.

Here {{color|orangemono|s}} and {{color|orangemono|t}} are PSL regular expressions.

{| class="wikitable"

| <code> s ; t </code>

Line 61 ⟶ 62:

| match of s followed by a match of t, t starts the same cycle that s ends

|-

| <sourcesyntaxhighlight lang="text" inline>s | t </sourcesyntaxhighlight>

| match of s or match of t

|-

Line 71 ⟶ 72:

|-

| <code> s within t </code>

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

|-

|}

Operators for consecutive repetitions are shown in the table below.

Here {{color|orangemono|s}} is a PSL regular expression.

{| class="wikitable"

| <code> s[*i] </code>

Line 96 ⟶ 97:

|}

Operators for non-consecutive repetitions are shown in the table below.

Here {{color|orangemono|b}} is any PSL Boolean expression.

{| class="wikitable"

| <code> b[=i] </code>

Line 104 ⟶ 105:

*equivalent to (!b[*];b)[*i]; !b[*]

|-

| <sourcesyntaxhighlight lang="text" inline> b[=i..j] </sourcesyntaxhighlight>

| at least i and mono more than j not necessarily consecutive repetitions of b,

*equivalent to (!b[*];b)[*i..j]; !b[*]

|-

Line 112 ⟶ 113:

*equivalent to (!b[*];b)[*i..]; !b[*]

|-

| <sourcesyntaxhighlight lang="text" inline> b[->m] </sourcesyntaxhighlight>

| m not necessarily consecutive repetitions of b ending with b,

*equivalent to (!b[*];b)[*m]

|-

| <code> b[->m:n] </code>

| at least m and mono more than n not necessarily consecutive repetitions of b ending with b,

*equivalent to (!b[*];b)[*m..n]

|-

| <code> b[->m..] </code>

| at least m not necessarily consecutive repetitions of b ending with b,

*equivalent to (!b[*];b)[*im..]; !b[*]

|-

| <code> b[->] </code>

Line 130 ⟶ 131:

|}

=== LTL-style Operatorsoperators===

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

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

{| class="wikitable"

| {{code|always p}}

| property p holds on every time point

|-

| {{code|never p}}

| property p does not holdshold on any time point

|-

| {{code|eventually! p}}

| there exists a future time point where p holds

|-

| {{code|next! p}}

| there exists a next time point, and p holds on this point

|-

| {{code|next p}}

| if there exists a next time point, then p holds on this point

|-

| {{code|next![n] p}}

| there exists an n-th time point, and p holds on this point

|-

| {{code|next[n] p}}

| if there exists an n-th time point, then p holds on this point

|-

| {{code|next_e![m..n] p}}

| there exists a time point, within m-th to n-th from the current where p holds.

|-

| {{code|next_e[m..n] p}}

| if there exists at least n-th time points, then p holds on one of the m-th to n-th points.

|-

| {{code|next_a![m..n] p}}

| there exists at least n more time points and p holds in all the time points between the m-th to the n-th, inclusive.

|-

| {{code|next_a[m..n] p}}

| p holds on all the next m-th through n-th time points, however many exist

|-

| {{code|p until! q}}

| there exists a time point where q holds, and p hold up until that time point

|-

| {{code|p until q}}

| p holds up until a time point where q hold, if such exists

|-

| {{code|p until!_ q}}

| there exists a time point where q holds, and p holdholds up until that time point and in that time point

|-

| {{code|p untiluntil_ q}}

| p holds up until a time point where q holdholds, and in that time point, if such exists

|-

| {{code|p before! q}}

| p holds strictly before the time point where q holds, and p eventually holds

|-

| {{code|p before q}}

| p holds strictly before the time point where q holds, if p never holds, then neither does q

|-

| {{code|p before!_ q}}

| p holds before or at the same time point where q holds, and p eventually holds

|-

| {{code|p before_ q}}

| p holds before or at the same time point where q holds, if p never holds, then neither does q

|-

|}

=== The Sampling Operatoroperator===

Sometimes it is desirable to change the definition of the ''next time-point'', for instance in multiply-clocked designs, or when a higher leverlevel of abstraction is desired. The ''sampling operator'' (a.k.aalso known as the ''the clock operator''), denoted {{color|redmono|@}}, is used for this purpose. The formula {{color|orangemono| p @ c }} where {{color|orangemono| p}} is a PSL formula and {{color|orangemono|c}} a PSL Boolean expressions holds on a given path if {{color|orangemono| p}} on that path projected on the cycles in which {{color|orangemono| 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 {{color|orangemono|request}} whichthat is immediately followed by an {{color|orangemono|ack}} signal, should be followed by a competecomplete {{color|orangemono|data transfer}}, where a complete data transfer is a sequence starting with signal {{color|orangemono|start}}, ending with signal {{color|orangemono|end}} in which {{color|orangemono|data}} should hold at least 8 times:

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

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

This is depicted in the second figure in which although the formula

<sourcesyntaxhighlight lang="text"> ((true[*]; req; ack) |=> (start; data[*3]; end)) @ clk </sourcesyntaxhighlight>

uses {{color|orangemono|data[*3]}} and {{color|orangemono|[*n]}} is consecutive repetition, the matching trace has 3 non-consecutive time points where {{color|orangemono|data}} holds, but when considering only the time points where {{color|orangemono|clk}} holds, the time points where {{color|orangemono|data}} hold become consecutive.

[[File:Multiple clocks.jpg|thumb|path and formula showing effect of the sampling operator @]]

The semantics of formulas with nested @ is a little subtle. The interested reader is referred to [2].

=== The Abort Operatorsoperators ===

PSL has several operators to deal with truncated paths (finite paths that may correspond to a prefix of the computation). Truncated paths occur in bounded-model checking, due to resets and in many other scenarios. The abort operators, specify how eventualities should be dealt with when a path has been truncated. They rely on the truncated semantics proposed in [1].

Here {{color|orangemono|p}} is any PSL formula and {{color|orangemono|b}} is any PSL Boolean expression.

{| class="wikitable"

| <code> p async_abort b </code>

| either p holds or p does not fail up until b holds, or p does not fail;

* b recognized asynchronously

|-

| <code> p sync_abort b </code>

| either p holds or p does not fail up until b holds, or p does not fail;

* b recognized synchronously

|-

Line 228 ⟶ 232:

|}

===Expressive Powerpower===

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 251 ⟶ 255:

*{{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|author2-link=Dana Fisman|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}}

*''Reasoning with Temporal Logic on Truncated Paths'', Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout

*{{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|author2-link=Dana Fisman|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}}

[http://www.research.ibm.com/people/e/eisner/papers/cav49.pdf] {{cite doi|10.1007/978-3-540-45069-6_3}}

*''The Definition of a Temporal Clock Operator'', Cindy Eisner, Dana Fisman, John Havlicek, Anthony McIsaac, David Van Campenhout

[http://www.cis.upenn.edu/~fisman/documents/EFHMV_ICALP03_full.pdf] {{cite doi|10.1007/3-540-45061-0_67}}

==External links==

* [http://www.eda.org/ieee-1850 IEEE 1850 working group]

* [https://web.archive.org/web/20051210035642/http://standards.ieee.org/announcements/pr_1850psl.html IEEE Announcement September 2005]

* [http://www.accellera.org/ Accellera]

* [http://www.project-veripage.com/psl_tutorial_1.php Property Specification Language Tutorial]

Line 265 ⟶ 267:

===Books on PSL===

* [http://www.systemverilog.us/psl_info.html Using PSL/Sugar for Formal and Dynamic Verification 2nd Edition, Ben Cohen, Ajeetha Kumari, Srinivasan Venkataramanan]

* [httphttps://www.springer.com/engineering/circuits+%26+systems/book/978-0-387-35313-5 A Practical Introduction to PSL], Cindy Eisner, and [[Dana Fisman]]

{{Programmable Logic}}

Line 273 ⟶ 275:

[[Category:Formal specification languages]]

[[Category:IEEE DASC standards]]

[[Category:IEC standards|#62531]]