View source for Property Specification Language

'''Property Specification Language''' ('''PSL''') is a [[Philosophy:Temporal logic|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|formal verification]] tools (such as [[Model checking|model checking]]) and/or  [[Engineering:Logic simulation|logic simulation]] tools are used to prove or refute that a given PSL formula holds on a given design.
PSL was initially developed by [[Organization:Accellera|Accellera]] for specifying [[Philosophy:Property|properties]] or assertions about hardware designs. Since September 2004 the standardization 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 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: 
<source lang="text">  always (request -> eventually! grant) 
</source>

The property "every  {{mono|request}} that 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: 
<source lang="text">  (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 lang="text">(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 ( {{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. The  {{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 (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.

Here {{mono|s}} and {{mono|t}} are PSL-regular expressions, and {{mono|p}} is a PSL formula.
 {| class="wikitable"
| <source lang="text"> s |=> t! </source> 
| 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
|-
| <source lang="text"> s |-> t! </source> 
| 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
|-
| <source lang="text"> s |=> t </source> 
| 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
|-
| <source lang="text"> s |-> t </source> 
| 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 may "get stuck" in the middle
|-
|}

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

Here {{mono|s}} and {{mono|t}} are PSL regular expressions.
{| class="wikitable"
| <code> s ; t </code> 
| match of s followed by a match of t, t starts the cycle after s ends
|-
| <code>s : t </code> 
| match of s followed by a match of t, t starts the same cycle that s ends
|-
| <source lang="text" inline>s | t </source> 
| match of s or match of t 
|-
| <code>s && t </code> 
| match of s and match of t, duration of both is of same length 
|-
| <code>s & t </code> 
| match of s and match of t, duration matches maybe different
|-
| <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 {{mono|s}} is a PSL regular expression. 
{| class="wikitable"
| <code> s[*i]  </code> 
| i consecutive repetitions of s
|-
| <code> s[*i..j] </code> 
| between i to j consecutive repetitions of s
|-
| <code> s[*i..] </code> 
| at least i to consecutive repetitions of s
|-
| <code> s[*] </code> 
| zero or more consecutive repetitions of s
|-
| <code> s[+] </code> 
| one or more consecutive repetitions of s
|-
|}

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

Here {{mono|b}} is any PSL Boolean expression. 
{| class="wikitable"
| <code> b[=i] </code> 
| i not necessarily consecutive repetitions of b, 
*equivalent to (!b[*];b)[*i]; !b[*]
|-
| <source lang="text" inline> b[=i..j] </source> 
| at least i  and no more than j not necessarily consecutive repetitions of b, 
*equivalent to (!b[*];b)[*i..j]; !b[*]
|-
| <code> b[=i..] </code> 
| at least i not necessarily consecutive repetitions of b, 
*equivalent to (!b[*];b)[*i..]; !b[*]
|-
| <source lang="text" inline> b[->m] </source> 
| m not necessarily consecutive repetitions of b ending with b, 
*equivalent to (!b[*];b)[*m]
|-
| <code> b[->m:n] </code> 
| at least m and no 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)[*m..]; !b[*]
|-
| <code> b[->] </code> 
| shortcut for b[->1], 
*equivalent to (!b[*];b)
|-
|}

=== LTL-style operators===

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

Here {{mono|p}} and {{mono|q}} are any PSL formulas.
{| class="wikitable"
| {{code|always p}}
| property p holds on every time point
|-
| {{code|never p}}
| property p does not hold 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 holds up until that time point and in that time point
|-
| {{code|p until_ q}}
| p holds up until a time point where q holds, 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
|-
|}

=== 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''  (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}} that 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: 
<source lang="text">  (true[*]; req; ack)  |=> (start; data[=8]; end) </source>
But sometimes it is desired to consider only the cases where the above signals occur on a cycle where {{mono|clk}} is high. 
This is depicted in the second figure in which although the formula 
<source lang="text">  ((true[*]; req; ack)  |=> (start; data[*3]; end)) @ clk </source>
uses  {{mono|data[*3]}} and {{mono|[*n]}} is consecutive repetition, the matching trace has 3 non-consecutive time points where {{mono|data}} holds, but when considering only the time points where {{mono|clk}} holds, the time points where {{mono|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].

=== Abort operators ===

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 {{mono|p}} is any PSL formula and {{mono|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; 

* b recognized asynchronously
|-
| <code> p sync_abort b </code> 
| either p holds or p does not fail up until b holds; 

* b recognized synchronously
|-
| <code> p abort b </code> 
| equivalent to p async_abort b
|-
|}

===Expressive power===
PSL subsumes the 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'', 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===
PSL is defined in 4 layers: the ''Boolean layer'', the ''temporal layer'', the ''modeling layer'' and the ''verification layer''.
*The ''Boolean layer'' is used for describing a current state of the design and is phrased using one of the above-mentioned HDLs.
*The ''temporal layer'' consists of the temporal operators used to describe scenarios that span over time (possibly over an unbounded number of time units).
*The ''modeling layer'' can be used to describe auxiliary state machines in a procedural manner.
*The ''verification layer'' consists of directives to a verification tool (for instance to ''assert'' that a given property is correct or to ''assume'' that a certain set of properties is correct when verifying another set of  properties).

===Language compatibility===
Property Specification Language can be used with multiple electronic system design languages (HDLs) such as:
* [[VHDL]] (IEEE 1076)
* [[Verilog]] (IEEE 1364)
* [[SystemVerilog]] (IEEE 1800)
* [[SystemC]] (IEEE 1666) by Open SystemC Initiative (OSCI).
When PSL is used in conjunction with one of the above HDLs, its Boolean layer uses the operators of the respective HDL.

==References==
*{{Cite book| title = 1850-2005 – IEEE Standard for Property Specification Language (PSL)| doi = 10.1109/IEEESTD.2005.97780| year = 2005| isbn = 0-7381-4780-X}}
**IEC 62531:2007 {{Cite book| title = 62531-2007 – IEC 62531 Ed. 1 (2007-11) (IEEE Std 1850-2005): Standard for Property Specification Language (PSL)| doi = 10.1109/IEEESTD.2007.4408637| year = 2007| isbn = 978-0-7381-5727-6}}
*{{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}}

==External links==
* [http://www.eda.org/ieee-1850 IEEE 1850 working group]
* [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]
* [http://www.doulos.com/knowhow/psl/ Designers guide to PSL]

===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]
* [https://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}}
{{IEEE standards}}

[[Category:Formal specification languages]]
[[Category:IEC standards]]

{{Sourceattribution|Property Specification Language}}