Property Specification Language
Verification language based on formal specification of behavior
Introduction to PSL
Property Specification Language (PSL) is a language for formal specification of electronic system behavior. These behaviors are captured as properties and can be executed as assertions within a logic simulator. PSL is a declarative language used to express temporal properties of the design, which means that it defines behavior over time.
PSL in a methodology
There are two primary ways in which PSL can be used. The first is within a simulation environment and it would generally be referred to as assertion-based verification (ABV). Assertions are used as inbuilt checkers that fire as soon as a behavior is identified that is not in conformance with the specification as encapsulated in a PSL property. This enables debugging to start at the point that a divergence is discovered rather than waiting for a manifestation of the problem to be seen at the external interface of the module or system being verified.
The second method is with static or formal verification tools. In a formal property checker, the tool would attempt to find any way in which the property can be violated. This provides a much high degree of verification than ABV because it is exhaustive. However, some tools may not be able to provide a definitive answer if the property is too complex or spans too great a period of time.
Variants of PSL
The PSL language was designed to be somewhat language independent, meaning independent of the language being used to describe the hardware. The variation is only syntactic in that PSL takes on the flavor of the hardware language, such as Verilog, VHDL or SystemC but does not alter the PSL semantics.
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).
A simple example of its usage is:
Assert (always req -> next (ack until grant)) @clk
This statement says that after the req signal becomes active, then on the next clk edge, ack must be active and stay active until the grant signal is active.
PSL belongs to a set of languages called temporal logic. These define the temporal, or time, based behavior of a system. They have existed for a long time in the mathematical domain but were complex languages and were not suitable for the development of electronics. One such language was called computation tree logic (CTL). The IBM Haifa Research Laboratory developed a layer on top of this language which they called sugar. This language evolved over time and when Accellera called for donations of property languages in 1998, IBM offered sugar. Accellera received several other donations and when they could not decide upon a single language on which to base PSL, IBM made some changes to sugar (Sugar 2.0) and it was accepted by the working group. PSL 1.0 was released in January 2003 and 1.01 released in April 2003.
Over the next year, the committee worked to align PSL with the assertion language that had been incorporated into SystemVerilog. This brought about closer syntactic and semantic alignment between the two languages and resulted in PSL 1.1 by June 2004. At this point it was turned over to the IEEE for continued work and ratification as IEEE 1850. It was released in In September 2005. As second IEEE version was released in 2010 and the IEC released their version of the standard IEC 62431 two years after each of the IEEE versions.
A Practical Introduction to PSL (Integrated Circuits and Systems) by Cindy Eisner, Dana Fisman. 2006
Using PSL/Sugar with Verilog and VHDL, Guide to Property Specification Language for ABV by Ben Cohen. 2003
- Other names: PSL, IEEE 1850
- Type: EDA
- Property Specification Language was invented by Accellera in 2003
IEEE 1850 is a ratification of Property Specification Language (2005)