Introduction to Formal Hardware Verification

Front Cover
Springer Science & Business Media, Oct 16, 1999 - Computers - 299 pages
Hardware verification is a hot topic in circuit and system design due to rising circuit complexity. This advanced textbook presents an almost complete overview of techniques for hardware verification. It covers all approaches used in existing tools, such as binary and word-level decision diagrams, symbolic methods for equivalence checking, and temporal logic model checking, and introduces the use of higher-order logic theorem proving for verifying circuit correctness. It enables the reader to understand the advantages and limitations of each technique. Each chapter contains an introduction and a summary as well as a section for the advanced reader. Thus a broad audience is addressed, from beginners in system design to experts.

From inside the book

Contents

Introduction
5
111 Faults and the Design Cycle
6
112 Avoiding Design Errors in Hardware Designs
7
12 Circuit Design
8
13 Fighting Design Errors
12
14 Verification versus Validation
14
151 Verification versus Simulation
15
152 Formal Specifications
16
352 Relational FSM Representation
107
353 Functional FSM Representation
118
354 State Space Traversal Variants
123
355 ROBDD Variable Ordering for FSM Equivalence Checking
136
356 Verification of Sequential Circuits without Reset Lines
137
357 Verification based Test Generation for Fabrication Faults
151
36 Summary
152
Propositional Temporal Logics
155

153 Formal Implementation Description
19
154 Correctness Relation and Proof
22
16 The Success of Formal Hardware Verification
25
161 Prerequisites for the Success of Hardware Verification
26
162 Properties of Successful Hardware Verification Approaches
27
17 Limitations of Formal Hardware Verification
29
110 Structure of the Book
32
Boolean Functions
35
22 Representations for Boolean Functions
36
221 Function Tables
37
222 Propositional Logic
38
223 Binary Decision Diagrams
41
23 Modeling Hardware Behavior
52
232 Relational Circuit Representation
53
233 Characteristic Functions
55
24 Specification Proof Goals and Proof
56
242 Explicit Hardware Verification
57
243 ModelBased Proof Approaches
59
252 Variable Ordering Heuristics
75
26 Technical Details
80
261 Classes of Boolean Functions
81
27 Summary
84
Approaches Based on Finite State Machines
87
32 Formal Basics
88
321 Automata for Finite Sequences
89
322 Automata for Infinite Sequences
93
323 Image and PreImage of a Function
94
33 Modeling Hardware Behavior
97
34 Specification Proof Goal and Proof
98
341 Symbolic State Machine Traversal
99
35 Further Developments
104
351 Structural Approaches to Circuit Equivalence
106
42 Formal Basics
157
422 The Propositional Temporal Logics CTL CTL and LTL
160
423 Comparing CTL LTL and CTL
168
424 Proof Algorithms
171
425 Comparing Proof Complexity
184
43 Modeling Hardware Behavior
187
431 Describing Implementations with Temporal Structures
188
432 Describing Implementations by Temporal Logic Formulas
192
441 Creating Temporal Logic Specifications
193
45 Further Developments
196
46 Technical Details
198
47 Summary
208
HigherOrder Logics
211
52 Formal Basics
213
522 First Order Logic
214
523 HigherOrder Logic
217
53 Modeling Hardware Behavior
229
532 Modeling Structures
231
55 Performing Proofs
232
551 Methodology for Establishing Circuit Correctness
233
552 Abstraction Mechanisms
239
553 Verification of Generic Circuits
246
56 Technical Details
249
562 Modeling Hardware Behavior
251
563 Formalizing Abstraction Mechanisms
253
57 Summary
257
Mathematical Basics
259
Axioms and Rules for CTL
271
Axioms and Rules for Higher Order Logic
275
References
281
Index
295
Copyright

Other editions - View all

Common terms and phrases

Popular passages

Page 282 - Ma, and AR Newton. On the verification of sequential machines at differing levels of abstraction.

Bibliographic information