Property Specification Language: Difference between revisions

Revision as of 09:57, 4 August 2015

Revision as of 10:01, 4 August 2015

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 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 ==