A Practical Introduction to PSL

1. Front Matter

   Pages I-XV

   PDF

2. Introduction

   Pages 1-4

3. Basic Temporal Properties

   Pages 5-17

4. Some Philosophy

   Pages 19-25

5. Weak vs. Strong Temporal Operators

   Pages 27-34

6. SERE Style

   Pages 35-63

7. Clocks

   Pages 65-82

8. Aborting a Property

   Pages 83-89

9. Some Convenient Constructs

   Pages 91-99

10. The Simple Subset

    Pages 101-102

11. The Boolean, Modeling, and Verification Layers

    Pages 103-107

12. Advanced Topics

    Pages 109-122

13. More Philosophy — High- vs. Low-level Assertions

    Pages 123-130

14. Common Errors

    Pages 131-160

15. Multiply-clocked Designs

    Pages 161-174

16. Back Matter

    Pages 175-240

    PDF

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.

• 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

• IBM Haifa Research Laboratory, Haifa, Israel

  Cindy Eisner

• The Weizmann Institute of Science, Rehovot, Israel

  Dana Fisman

Policies and ethics