A Practical Introduction to PSL
Buch in deiner Nähe kaufen
Beschreibung
A Practical Introduction to PSL describes the Property Specification Language PSL, recently standardized as IEEE Std 1850-2005. PSL provides a way to express properties of a design. Both authors, Cindy Eisner (IBM Haifa Research Laboratory, Haifa University Campus, Haifa, Israel) and Dana Fisman (The Weizmann Institute of Science, Rehovot, Israel) were involved with the creation of the standard.
A Practical Introduction to PSL includes extensive examples illustrated with timing diagrams. While mostly oriented to users of PSL for simulation, a section on the use of PSL in formal verification is included. All of the basic language constructs are covered, as well as advanced topics such as the use of PSL in multiply-clocked designs. The chapter on common errors, based on the authors’ many years of experience in using and teaching the language, will be helpful to both beginners and more experienced users.
A Practical Introduction to PSL is primarily targeted to hardware designers and verification engineers who plan to use PSL. This book is also of interest to students of temporal logic. The formal semantics of PSL are included as an appendix, and bibliographical notes include pointers to some of the main theoretical works.
______________________________________________________
From the Foreword:
… "Cindy Eisner and Dana Fisman were the two key people who turned IBM Sugar into PSL. Their deep understanding of PSL’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
This book describes the Property Specification Language PSL, recently standardized as IEEE Standard 1850-2005. The text presents PSL using extensive examples in the form of timing diagrams and associated PSL properties, with a full chapter devoted to avoiding common errors.
Functional veri?cation is hard. Period. No disagreement here. But why is this so? Consider today’s design ?ow: much of it is more or less automated, from RTL to netlist to layout to silicon. But all this automation depends upon having correct RTL input to start with, and there is little or no automation to help with RTL creation. It is hard enough for a designer to decide what RTL model he wants to build, and then to describe that RTL model correctly in a hardware description language. It is even more di?cult for a veri?cation engineer, who can’t read the designer’s mind, to verify that what the designer created not only represents the RTL model he had conceived, but also that the RTL model is an appropriate one for the problem at hand. What makes RTL modeling and veri?cation di?cult is concurrency. It is easy to teach an engineer how to write procedural code that conforms to the synthesizable subset of a hardware description language. What is hard is understanding how the engineer’s procedural code interacts with other c- ponents in the design over time. In fact, until recently we lacked e?ective languages to describe concurrent behaviors. The IEEE 1850 Property Speci?cation Language (PSL) is a language for the formal speci?cation of concurrent systems. The language is particularly applicable for writing assertions about hardware designs. PSL supports m- tiple veri?cation paradigms – including formal analysis, simulation, and acc- eration/emulation.
Presents assertion-based verification using the IEEE Property Specification Language (PSL), an emerging industry standard, based on IBM's Sugar 2.0 assertion language
Includes actual designs using assertion PSL
This book describes the Property Specification Language PSL, recently standardized as IEEE Standard 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. The text presents PSL using extensive examples in the form of timing diagrams and associated PSL properties. Primarily oriented to users of PSL for simulation, it also addresses formal verification. 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. A full chapter is devoted to errors commonly made by beginners, gathered through the authors' many years of experience in using and teaching the language.
Autor*in
Cindy Eisner
Themen in »A Practical Introduction to PSL«
Assertion Languages Assertion-Based Verification Formal property specification Simulation and formal verification Standard Temporal logic algorithms computer-aided design (CAD) layers logic modeling semantics simulation