Introduction to PSL

Ensuring that a design's implementation satisfies its specification is the foundation of hardware verification. Key to the design and verification process is the act of specification. Yet historically, the process of specification has consisted of creating a natural language description of a set of design requirements. This form of specification is both ambiguous and, in many cases, unverifiable due to the lack of a standard machine-executable representation. Furthermore, ensuring that all functional aspects of the specification have been adequately verified (that is, covered) is problematic. The IEEE Property Specification Language (PSL) was developed to address these shortcomings. It gives the design architect a standard means of specifying design properties using a concise syntax with clearly-defined formal semantics. Similarly, it enables the RTL implementer to capture design intent in a verifiable form, while enabling the verification engineer to validate that the implementation satisfies its specification through dynamic (that is, simulation) and static (that is, formal) verification means.
Furthermore, it provides a means to measure the quality of the verification process through the creation of functional coverage models built on formally specified properties. Plus, it provides a standard means for hardware designers and verification engineers to rigorously document the design specification (machine-executable). PSL was specifically developed to fulfill the following general hardware functional specification requirements: easy to learn, write, and read; concise syntax; rigorously well-defined formal semantics; expressive power, permitting the specification for a large class of real world design properties; and, known efficient underlying algorithms in simulation, as well as formal verification This book presents assertion-based verification using the IEEE Property Specification Language (PSL), an emerging industry standard, based on IBM's Sugar 2.0 assertion language. We begin with the general concept of assertions and an overview of various languages that have been used to express assertions. Next, we introduce PSL.
We review the temporal logic concepts upon which PSL is based, and we present the rich layered structure of the language, in particular the layer which supports temporal assertions based on linear temporal logic (LTL). Next, we present a methodology for applying assertions, including use of assertions for interface checking, constraint specification, internal consistency checking, and coverage monitoring, using PSL as a vehicle to illustrate the concepts. We discuss how assertions can be used in a wide range of verification flows including static analysis, simulation, emulation, and test generation. Next, we review developing support for PSL in the industry and describe how PSL enables an assertion-based methodology built upon interoperable tools. We demonstrate the use of assertions through assertion-based verification of a small design example. We finish with a summary of experience with the use of assertions PSL in actual designs.