Content deleted Content added
m WP:CHECKWIKI error fix. Section heading problem. Violates WP:MOSHEAD. |
move "history" to lead |
||
Line 1:
'''Property Specification Language''' ('''PSL''') is a language developed by [[Accellera]] for specifying [[Property (philosophy)|properties]] or [[assertion (computing)|assertions]] about hardware designs. The properties can then be [[functional verification|functionally verified]] via [[logic simulation]] or [[formal verification]]. 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.▼
''Property Specification Language (PSL)'', is a temporal logic extending [[Linear temporal logic|(LTL)]] 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]]) are used to prove or refute that a given PSL formula holds on a given design. ▼
▲
== Examples ==
Line 231 ⟶ 233:
===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'', 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.
▲'''Property Specification Language''' ('''PSL''') is a language developed by [[Accellera]] for specifying [[Property (philosophy)|properties]] or [[assertion (computing)|assertions]] about hardware designs. The properties can then be [[functional verification|functionally verified]] via [[logic simulation]] or [[formal verification]]. 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.
===Layers===
| |||