Content deleted Content added
No edit summary |
cap, bold, simplify heaidng |
||
Line 1:
'''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 [[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
PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a {{color|orange|request}} should always eventually be {{color|orange|grant}} ed" can be expressed by the PSL formula:
Line 130:
|}
=== LTL-style
Below is a sample of some LTL-style operators of PSL.
Line 195:
|}
===
Sometimes it is desirable to change the definition of the ''next time-point'', for instance in multiply-clocked designs, or when a higher lever of abstraction is desired. The ''sampling operator'' (a.k.a ''the clock operator''), denoted {{color|red|@}}, is used for this purpose. The formula {{color|orange| p @ c }} where {{color|orange| p}} is a PSL formula and {{color|orange|c}} a PSL Boolean expressions holds on a given path if {{color|orange| p}} on that path projected on the cycles in which {{color|orange| c}} holds, as exemplified in the figures to the right.
Line 209:
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].
Line 228:
|}
===Expressive
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. ''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.
| |||