Property Specification Language

From Wikipedia, the free encyclopedia
Jump to: navigation, search

Property Specification Language (PSL) is a language developed by Accellera for specifying properties or assertions about hardware designs. The properties can then be functionally verified via logic simulation or formal verification. 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.

Property Specification Language aims to be used with multiple electronic system design languages (HDLs) such as:


PSL is a declarative language used to express temporal properties of the design. For instance, PSL can express the property "a request should always be granted within five cycles unless an abort signal was issued". Formal verification tools (such as model checking) can be used to prove or refute that a given PSL formula holds on a given design.

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).

PSL subsumes the temporal logic LTL and extends its expressive power to that of the omega-regular languages. PSL makes an extensive use of regular expressions and syntactic sugaring. 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.


External links[edit]

Books on PSL[edit]