Property Specification Language (PSL) is atemporal logic extendinglinear temporal logic with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use ofregular expressions and syntactic sugaring. It is widely used in the hardware design and verification industry, whereformal verification tools (such asmodel checking) and/orlogic simulation tools are used to prove or refute that a given PSL formula holds on a given design.
PSL was initially developed byAccellera for specifyingproperties orassertions about hardware designs. Since September 2004 thestandardization on the language has been done inIEEE 1850 working group. In September 2005, the IEEE 1850 Standard for Property Specification Language (PSL) was announced.
PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "arequest should always eventually begranted" can be expressed by the PSL formula:
always (request -> eventually! grant)
The property "everyrequest that is immediately followed by anack signal, should be followed by a completedata transfer, where a complete data transfer is a sequence starting with signalstart, ending with signalend in whichbusy holds at the meantime" can be expressed by the PSL formula:
(true[*]; req; ack) |=> (start; busy[*]; end)
A trace satisfying this formula is given in the figure on the right.
(true[*]; req; ack) |=> (start; busy[*]; end)
PSL's temporal operators can be roughly classified intoLTL-style operators andregular-expression-style operators. Many PSL operators come in two versions, a strong version, indicated by an exclamation mark suffix (! ), and a weak version. Thestrong version makes eventuality requirements (i.e. require that something will hold in the future), while theweak version does not. Anunderscore suffix (_ ) is used to differentiateinclusive vs.non-inclusive requirements. The_a and_e suffixes are used to denoteuniversal (all) vs.existential (exists) requirements. Exact time windows are denoted by[n] and flexible by[m..n].
The most commonly used PSL operator is the "suffix-implication" operator (also known as the "triggers" operator), which is denoted by|=>. 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 ofr |=> 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.
The regular expressions of PSL have the common operators for concatenation (;), Kleene-closure (*), and union (|), as well as operator for fusion (:), intersection (&&) and a weaker version (&), and many variations for consecutive counting[*n] and in-consecutive counting e.g.[=n] and[->n].
The trigger operator comes in several variations, shown in the table below.
Heres andt are PSL-regular expressions, andp is a PSL formula.
s |=> t! | if there is a match of s, then there is a match of t on the suffix of the trace,
|
s |-> t! | if there is a match of s, then there is a match of t on the suffix of the trace,
|
s |=> t | if there is a match of s, then there is a match of t on the suffix of the trace,
|
s |-> t | if there is a match of s, then there is a match of t on the suffix of the trace,
|
Operators for concatenation, fusion, union, intersection and their variations are shown in the table below.
Heres andt are PSL regular expressions.
s ; t | match of s followed by a match of t, t starts the cycle after s ends |
s : t | match of s followed by a match of t, t starts the same cycle that s ends |
s | t | match of s or match of t |
s && t | match of s and match of t, duration of both is of same length |
s & t | match of s and match of t, duration matches maybe different |
s within t | match of s within a match of t, abbreviation of ([*]; s; [*]) && t |
Operators for consecutive repetitions are shown in the table below.
Heres is a PSL regular expression.
s[*i] | i consecutive repetitions of s |
s[*i..j] | between i to j consecutive repetitions of s |
s[*i..] | at least i to consecutive repetitions of s |
s[*] | zero or more consecutive repetitions of s |
s[+] | one or more consecutive repetitions of s |
Operators for non-consecutive repetitions are shown in the table below.
Hereb is any PSL Boolean expression.
b[=i] | i not necessarily consecutive repetitions of b,
|
b[=i..j] | at least i and no more than j not necessarily consecutive repetitions of b,
|
b[=i..] | at least i not necessarily consecutive repetitions of b,
|
b[->m] | m not necessarily consecutive repetitions of b ending with b,
|
b[->m:n] | at least m and no more than n not necessarily consecutive repetitions of b ending with b,
|
b[->m..] | at least m not necessarily consecutive repetitions of b ending with b,
|
b[->] | shortcut for b[->1],
|
Below is a sample of some LTL-style operators of PSL.
Herep andq are any PSL formulas.
always p | property p holds on every time point |
never p | property p does not hold on any time point |
eventually! p | there exists a future time point where p holds |
next! p | there exists a next time point, and p holds on this point |
next p | if there exists a next time point, then p holds on this point |
next![n] p | there exists an n-th time point, and p holds on this point |
next[n] p | if there exists an n-th time point, then p holds on this point |
next_e![m..n] p | there exists a time point, within m-th to n-th from the current where p holds. |
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. |
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. |
next_a[m..n] p | p holds on all the next m-th through n-th time points, however many exist |
p until! q | there exists a time point where q holds, and p hold up until that time point |
p until q | p holds up until a time point where q hold, if such exists |
p until!_ q | there exists a time point where q holds, and p holds up until that time point and in that time point |
p until_ q | p holds up until a time point where q holds, and in that time point, if such exists |
p before! q | p holds strictly before the time point where q holds, and p eventually holds |
p before q | p holds strictly before the time point where q holds, if p never holds, then neither does q |
p before!_ q | p holds before or at the same time point where q holds, and p eventually holds |
p before_ q | p holds before or at the same time point where q holds, if p never holds, then neither does q |
Sometimes it is desirable to change the definition of thenext time-point, for instance in multiply-clocked designs, or when a higher level of abstraction is desired. Thesampling operator (also known as theclock operator), denoted@, is used for this purpose. The formula p @ c where p is a PSL formula andc a PSL Boolean expressions holds on a given path if p on that path projected on the cycles in which c holds, as exemplified in the figures to the right.
The first property states that "everyrequest that is immediately followed by anack signal, should be followed by a completedata transfer, where a complete data transfer is a sequence starting with signalstart, ending with signalend in whichdata should hold at least 8 times:
(true[*]; req; ack) |=> (start; data[=8]; end)
But sometimes it is desired to consider only the cases where the above signals occur on a cycle whereclk is high. This is depicted in the second figure in which although the formula
((true[*]; req; ack) |=> (start; data[*3]; end)) @ clk
usesdata[*3] and[*n] is consecutive repetition, the matching trace has 3 non-consecutive time points wheredata holds, but when considering only the time points whereclk holds, the time points wheredata hold become consecutive.
The semantics of formulas with nested @ is a little subtle. The interested reader is referred to [2].
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].
Herep is any PSL formula andb is any PSL Boolean expression.
p async_abort b | either p holds or p does not fail up until b holds;
|
p sync_abort b | either p holds or p does not fail up until b holds;
|
p abort b | equivalent to p async_abort b |
PSL subsumes the temporal logicLTL and extends its expressive power to that of theomega-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 thesuffix implication, also known as thetriggers operator, denoted "|->". The formular |-> f wherer is a regular expression andf is a temporal logic formula holds on a computationw if any prefix ofw matchingr has a continuation satisfyingf. Other non-LTL operators of PSL are the@ operator, for specifying multiply-clocked designs, theabort operators, for dealing with hardware resets, andlocal variables for succinctness.
PSL is defined in 4 layers: theBoolean layer, thetemporal layer, themodeling layer and theverification layer.
Property Specification Language can be used with multiple electronic system design languages (HDLs) such as:
When PSL is used in conjunction with one of the above HDLs, its Boolean layer uses the operators of the respective HDL.
