Property Specification Language

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:

• VHDL (IEEE 1076),
• Verilog (IEEE 1364),
• SystemVerilog (IEEE 1800), and
• SystemC (IEEE 1666) by Open SystemC Initiative (OSCI).

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.

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. 

External links

• IEEE 1850 working group
• IEEE Announcement September 2005
• Accellera
• Property Specification Language Tutorial
• Designers guide to PSL

Books on PSL

• Using PSL/Sugar for Formal and Dynamic Verification 2nd Edition, Ben Cohen, Ajeetha Kumari, Srinivasan Venkataramanan
• A Practical Introduction to PSL, Cindy Eisner, Dana Fisman