KnowHow
Free Technical Resources

PSL was chartered by the Functional Verification Technical Committee of Accellera. After a process in which donations from a number of sources were evaluated, the Sugar language from IBM was chosen as the basis for PSL. The Language Reference Manual for PSL version 1.01 was released in April 2003. PSL Version 1.1 was under development as of February 2004.

Sugar began as an internal development within IBM, where the CTL formalism (Computation Tree Logic) was used to express properties for model checking. The raw CTL notation allows the concise expression of temporal relationships, but was found hard to write and read by non-specialists. Sugar was developed to provide syntactic sugaring on top of CTL, i.e. a layer of user-friendly syntax to hide the more obscure notation. Sugar was subsequently extended to support sequential regular expressions, an extension of the regular expressions familiar to Unix and Perl programmers into the time domain, which provided an alternative form of syntactic sugaring. An implementation of dynamic property checking during simulation was added, and finally the underlying semantic foundation was migrated from CTL to LTL (Linear-time Temporal Logic), because the latter was considered more suitable for simulation and accessible to a wider audience.

PSL currently provides the raw CTL and LTL operators, together with two forms of syntactic sugaring: the temporal operators of the Foundation Language (FL), and Sequential Extended Regular Expressions (SERE). The semantics of each are formally defined in the PSL Language Reference Manual.

The PSL standard is currently owned by Accellera. The PSL/Sugar Consortium is a complementary organisation that exists to facilitate the adoption of PSL by the user community.

 

Next: The Structure of PSL