A Practical Introduction to PSL (eBook)
XVI, 240 Seiten
Springer US (Verlag)
978-0-387-36123-9 (ISBN)
This book describes the Property Specification Language PSL, recently standardized as IEEE Standard 1850-2005. PSL was 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. Basic features are covered, as well as advanced topics such as the use of PSL in multiply-clocked designs. A full chapter is devoted to common errors, gathered through the authors' many years of experience in using and teaching the language.
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.
Foreword 7
Preface 9
Contents 11
1 Introduction 16
2 Basic Temporal Properties 20
3 Some Philosophy 33
4 Weak vs. Strong Temporal Operators 40
5 SERE Style 48
6 Clocks 77
7 Aborting a Property 95
8 Some Convenient Constructs 102
9 The Simple Subset 111
10 The Boolean, Modeling, and Verification Layers 113
11 Advanced Topics 118
12 More Philosophy – High- vs. Low-level Assertions 132
13 Common Errors 140
14 Multiply-clocked Designs 170
A Syntax Rule Summary 184
B Formal Syntax and Semantics 200
C Operator Precedence 212
D Quick Reference 213
Bibliographic Notes 232
References 237
Index 241
Erscheint lt. Verlag | 19.6.2007 |
---|---|
Reihe/Serie | Integrated Circuits and Systems | Integrated Circuits and Systems |
Zusatzinfo | XVI, 240 p. |
Verlagsort | New York |
Sprache | englisch |
Themenwelt | Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge |
Informatik ► Weitere Themen ► CAD-Programme | |
Technik ► Elektrotechnik / Energietechnik | |
Schlagworte | algorithms • Assertion-based verification • Assertion Languages • Computer-Aided Design (CAD) • Formal property specification • Layers • Logic • Modeling • Semantics • Simulation • Simulation and formal verification • Standard • temporal logic |
ISBN-10 | 0-387-36123-5 / 0387361235 |
ISBN-13 | 978-0-387-36123-9 / 9780387361239 |
Haben Sie eine Frage zum Produkt? |
![PDF](/img/icon_pdf_big.jpg)
Größe: 1,6 MB
DRM: Digitales Wasserzeichen
Dieses eBook enthält ein digitales Wasserzeichen und ist damit für Sie personalisiert. Bei einer missbräuchlichen Weitergabe des eBooks an Dritte ist eine Rückverfolgung an die Quelle möglich.
Dateiformat: PDF (Portable Document Format)
Mit einem festen Seitenlayout eignet sich die PDF besonders für Fachbücher mit Spalten, Tabellen und Abbildungen. Eine PDF kann auf fast allen Geräten angezeigt werden, ist aber für kleine Displays (Smartphone, eReader) nur eingeschränkt geeignet.
Systemvoraussetzungen:
PC/Mac: Mit einem PC oder Mac können Sie dieses eBook lesen. Sie benötigen dafür einen PDF-Viewer - z.B. den Adobe Reader oder Adobe Digital Editions.
eReader: Dieses eBook kann mit (fast) allen eBook-Readern gelesen werden. Mit dem amazon-Kindle ist es aber nicht kompatibel.
Smartphone/Tablet: Egal ob Apple oder Android, dieses eBook können Sie lesen. Sie benötigen dafür einen PDF-Viewer - z.B. die kostenlose Adobe Digital Editions-App.
Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook-orders from other countries.
aus dem Bereich