Property Specification Language

Last updated March 21, 2023

Property Specification Language (PSL) is a 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 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 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 request should always eventually be granted" can be expressed by the PSL formula:

  always (request -> eventually! grant)

The property "every request that is immediately followed by an ack signal, should be followed by a complete data transfer, where a complete data transfer is a sequence starting with signal start, ending with signal end in which busy 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.

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

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.

Here s and t are PSL-regular expressions, and p 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, t starts the cycle after s ends, the match of t must reach to its end
s \|-> t!	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
s \|=> t	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
s \|-> t	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 s and t 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.

Here s 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.

Here b is any PSL Boolean expression.

`b[=i]`	i not necessarily consecutive repetitions of b, equivalent to (!b[];b)[i]; !b[*]
`b[=i..j]`	at least i and no more than j not necessarily consecutive repetitions of b, equivalent to (!b[];b)[i..j]; !b[*]
`b[=i..]`	at least i not necessarily consecutive repetitions of b, equivalent to (!b[];b)[i..]; !b[*]
`b[->m]`	m not necessarily consecutive repetitions of b ending with b, equivalent to (!b[];b)[m]
`b[->m:n]`	at least m and no more than n not necessarily consecutive repetitions of b ending with b, equivalent to (!b[];b)[m..n]
`b[->m..]`	at least m not necessarily consecutive repetitions of b ending with b, equivalent to (!b[];b)[m..]; !b[*]
`b[->]`	shortcut for b[->1], equivalent to (!b[*];b)

LTL-style operators

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

Here p and q 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

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 @, is used for this purpose. The formula p @ c where p is a PSL formula and c 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 "every request that is immediately followed by an ack signal, should be followed by a complete data transfer, where a complete data transfer is a sequence starting with signal start, ending with signal end in which data 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 where clk is high. This is depicted in the second figure in which although the formula

  ((true[*]; req; ack)  |=> (start; data[*3]; end)) @ clk

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

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 p is any PSL formula and b is any PSL Boolean expression.

`p async_abort b`	either p holds or p does not fail up until b holds; b recognized asynchronously
`p sync_abort b`	either p holds or p does not fail up until b holds; b recognized synchronously
`p abort b`	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.

Related Research Articles

The VHSIC Hardware Description Language (VHDL) is a hardware description language (HDL) that can model the behavior and structure of digital systems at multiple levels of abstraction, ranging from the system level down to that of logic gates, for design entry, documentation, and verification purposes. Since 1987, VHDL has been standardized by the Institute of Electrical and Electronics Engineers (IEEE) as IEEE Std 1076; the latest version of which is IEEE Std 1076-2019. To model analog and mixed-signal systems, an IEEE-standardized HDL based on VHDL called VHDL-AMS has been developed.

Verilog, standardized as IEEE 1364, is a hardware description language (HDL) used to model electronic systems. It is most commonly used in the design and verification of digital circuits at the register-transfer level of abstraction. It is also used in the verification of analog circuits and mixed-signal circuits, as well as in the design of genetic circuits. In 2009, the Verilog standard was merged into the SystemVerilog standard, creating IEEE Standard 1800-2009. Since then, Verilog is officially part of the SystemVerilog language. The current version is IEEE standard 1800-2017.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a modal logic-based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians.

Standard Delay Format (SDF) is an IEEE standard for the representation and interpretation of timing data for use at any stage of an electronic design process. It finds wide applicability in design flows, and forms an efficient bridge between dynamic timing verification and static timing analysis.

In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers. LTL is sometimes called propositional temporal logic, abbreviated PTL. In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic.

Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers, which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied, then all possible executions of a program avoid some undesirable condition. In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic belongs to a class of temporal logics that includes linear temporal logic (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in CTL*.

A test plan is a document detailing the objectives, resources, and processes for a specific test for a software or hardware product. The plan typically contains a detailed understanding of the eventual workflow.

SystemVerilog, standardized as IEEE 1800, is a hardware description and hardware verification language used to model, design, simulate, test and implement electronic systems. SystemVerilog is based on Verilog and some extensions, and since 2008, Verilog is now part of the same IEEE standard. It is commonly used in the semiconductor and electronic design industry as an evolution of Verilog.

CTL* is a superset of computational tree logic (CTL) and linear temporal logic (LTL). It freely combines path quantifiers and temporal operators. Like CTL, CTL* is a branching-time logic. The formal semantics of CTL* formulae are defined with respect to a given Kripke structure.

Unified Power Format (UPF) is the popular name of the Institute of Electrical and Electronics Engineers (IEEE) standard for specifying power intent in power optimization of electronic design automation. The IEEE 1801-2009 release of the standard was based on a donation from the Accellera organization. The current release is IEEE 1801-2018.

IP-XACT is an XML format that defines and describes individual, re-usable electronic circuit designs to facilitate their use in creating integrated circuits. IP-XACT was created by the SPIRIT Consortium as a standard to enable automated configuration and integration through tools.

CADP is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.

High-level verification (HLV), or electronic system-level (ESL) verification, is the task to verify ESL designs at high abstraction level, i.e., it is the task to verify a model that represents hardware above register-transfer level (RTL) abstract level. For high-level synthesis, HLV is to HLS as functional verification is to logic synthesis.

TLA⁺ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA⁺ is considered to be exhaustively-testable pseudocode, and its use likened to drawing blueprints for software systems; TLA is an acronym for Temporal Logic of Actions.

In formal verification, finite state model checking needs to find a Büchi automaton (BA) equivalent to a given linear temporal logic (LTL) formula, i.e., such that the LTL formula and the BA recognize the same ω-language. There are algorithms that translate an LTL formula to a BA. This transformation is normally done in two steps. The first step produces a generalized Büchi automaton (GBA) from a LTL formula. The second step translates this GBA into a BA, which involves a relatively easy construction. Since LTL is strictly less expressive than BA, the reverse construction is not always possible.

Metric temporal logic (MTL) is a special case of temporal logic. It is an extension of temporal logic in which temporal operators are replaced by time-constrained versions like until, next, since and previous operators. It is a linear-time logic that assumes both the interleaving and fictitious-clock abstractions. It is defined over a point-based weakly-monotonic integer-time semantics.

<i>Principles of Model Checking</i> Computer science textbook

Principles of Model Checking is a textbook on model checking, an area of computer science that automates the problem of determining if a machine meets specification requirements. It was written by Christel Baier and Joost-Pieter Katoen, and published in 2008 by MIT Press.

References

1850-2005 – IEEE Standard for Property Specification Language (PSL). 2005. doi:10.1109/IEEESTD.2005.97780. ISBN 0-7381-4780-X.
- IEC 62531:2007 62531-2007 – IEC 62531 Ed. 1 (2007-11) (IEEE Std 1850-2005): Standard for Property Specification Language (PSL). 2007. doi:10.1109/IEEESTD.2007.4408637. ISBN 978-0-7381-5727-6.
1850-2010 – IEEE Standard for Property Specification Language (PSL). 2010. doi:10.1109/IEEESTD.2010.5446004. ISBN 978-0-7381-6255-3.
- IEC 62531:2012 62531-2012 – IEC 62531:2012(E) (IEEE Std 1850-2010): Standard for Property Specification Language (PSL). 2012. doi:10.1109/IEEESTD.2012.6228486. ISBN 978-0-7381-7299-6.
Eisner, Cindy; Fisman, Dana; Havlicek, John; Lustig, Yoad; McIsaac, Anthony; Van Campenhout, David (2003). "Reasoning with Temporal Logic on Truncated Paths" (PDF). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 2725. p. 27. doi:10.1007/978-3-540-45069-6_3. ISBN 978-3-540-40524-5.
Eisner, Cindy; Fisman, Dana; Havlicek, John; McIsaac, Anthony; Van Campenhout, David (2003). "The Definition of a Temporal Clock Operator" (PDF). Automata, Languages and Programming. Lecture Notes in Computer Science. Vol. 2719. p. 857. doi:10.1007/3-540-45061-0_67. ISBN 978-3-540-40493-4.

External links

Books on PSL

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.