A Practical Introduction to PSL

This book describes the Property Specification Language PSL, recently standardized as IEEE Std 1850-2005. PSL was specifically developed to fulfill the following 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 - known efficient underlying algorithms in simulation, as well as formal verification This book is primarily targeted to hardware designers and verification engineers who plan to use PSL. It presents PSL using extensive examples in the form of timing diagrams and associated PSL properties. In addition to language elements, it touches on methodological issues in the use of PSL. While primarily oriented to users of PSL for simulation, formal verification is addressed as well. All the basic features of the language are covered, as well as advanced topics such as the use of PSL in multiply-clocked designs and the issue of embedding asynchronous properties in synchronous ones. One chapter is devoted to errors commonly made by begi nners gathered through the authors' many years of experience in using and teaching the language, and will be helpful to both beginners and more experienced users. The book is accessible to the typical hardware designer and verification engineer with no interest in the theory behind temporal logic. However, the formal semantics are included as an appendix, so that those with such an interest will be able to refer to them. From the Foreword: a?| "Cindy Eisner and Dana Fisman were the two key people who turned IBM Sugar into PSL. Their deep understanding of PSLa's formal semantics was instrumental in both the Accellera and IEEE PSL standardization efforts. Cindy and Dana have now created the most authoritative source for information about PSL, designed to introduce the language incrementally in an easily understood fashion. A Practical Introduction to PSL provides a solid foundation for getting started with PSL today." Harry Foster - Erich Marschner Mentor Graphics Corporation Cadence Design Systems