A Practical Introduction to PSL
- 3h 4m
- Cindy Eisner, Dana Fisman
- Springer
- 2006
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 beginners 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.
In this Book
-
Introduction
-
Basic Temporal Properties
-
Some Philosophy
-
Weak vs. Strong Temporal Operators
-
SERE Style
-
Clocks
-
Aborting a Property
-
Some Convenient Constructs
-
The Simple Subset
-
The Boolean, Modeling, and Verification Layers
-
Advanced Topics
-
More Philosophy — High- vs. Low-Level Assertions
-
Common Errors
-
Multiply-Clocked Designs
-
Bibliographic Notes