The PSL/Sugar specification language: A language for all seasons

Abstract

The Accellera EDA standards body has recently approved the PSL a standard property specification language for use in assertion-based verification via simulation and formal verification tools. This language, which is based on the Sugar language from IBM, is now supported by many EDA vendors. More than 40 individuals representing over 20 companies participated in the efforts to form the PSL standard from its Sugar basis. The tutorial comprises 2 parts. In the first part, we describe the basic principles of PSL/Sugar, focusing on the ease with which complex design behaviors may be described with concise, readable PSL/Sugar assertions that crisply capture design intent. We summarize the temporal constructs of the language, including parameterized sequences and properties, directives, and modeling capabilities. We cover the general timing model of PSL/Sugar, which transparently supports both (single-or multi-clock) synchronous and asynchronous design, and, time permitting, we explain how PSL/Sugar has been defined to ensure consistent semantics for both simulation and formal verification applications. In the second part of the tutorial, we present several applications of PSL/Sugar, ranging from simple to advanced assertion-based verification solutions. These include use of PSL/Sugar for dynamic assertion checking and formal model checking, including support for environment modeling and assume/guarantee reasoning. Examples of commercial verification tools which support the PSL/Sugar languages will also be presented. Participants in the tutorial will have an excellent opportunity to learn about both the language and its applications directly from the speaker, Dr. Danny Geist, who heads a research group in the IBM Haifa lab where Sugar was conceived. © Springer-Verlag Berlin Heidelberg 2003.