Editing Property Specification Language (section)

== 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}} 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: 
<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. 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"
| <syntaxhighlight lang="text"> s |=> t! </syntaxhighlight> 
| 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
|-
| <syntaxhighlight lang="text"> s |-> t! </syntaxhighlight> 
| 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
|-
| <syntaxhighlight lang="text"> s |=> t </syntaxhighlight> 
| 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
|-
| <syntaxhighlight lang="text"> s |-> t </syntaxhighlight> 
| 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
|-
| <syntaxhighlight lang="text" inline>s | t </syntaxhighlight> 
| 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[*]
|-
| <syntaxhighlight lang="text" inline> b[=i..j] </syntaxhighlight> 
| 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[*]
|-
| <syntaxhighlight lang="text" inline> b[->m] </syntaxhighlight> 
| 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: 
<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. 
This is depicted in the second figure in which although the formula 
<syntaxhighlight lang="text">  ((true[*]; req; ack)  |=> (start; data[*3]; end)) @ clk </syntaxhighlight>
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 [[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'', 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|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.