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.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Introduction
1
111 Faults and the Design Cycle
2
112 Avoiding Design Errors in Hardware Designs
3
12 Circuit Design
4
13 Fighting Design Errors
8
14 Verification versus Validation
10
151 Verification versus Simulation
11
152 Formal Specifications
12
352 Relational FSM Representation
103
353 Functional FSM Representation
114
354 State Space Traversal Variants
119
355 ROBDD Variable Ordering for FSM Equivalence Checking
132
356 Verification of Sequential Circuits without Reset Lines
133
357 Verification based Test Generation for Fabrication Faults
147
36 Summary
148
Propositional Temporal Logics
151

153 Formal Implementation Description
15
154 Correctness Relation and Proof
18
16 The Success of Formal Hardware Verification
21
161 Prerequisites for the Success of Hardware Verification
22
162 Properties of Successful Hardware Verification Approaches
23
17 Limitations of Formal Hardware Verification
25
18 The Pragmatic Approach Recipes for Verifying Circuits
26
110 Structure of the Book
28
Boolean Functions
31
22 Representations for Boolean Functions
32
221 Function Tables
33
222 Propositional Logic
34
223 Binary Decision Diagrams
37
23 Modeling Hardware Behavior
48
232 Relational Circuit Representation
49
233 Characteristic Functions
51
24 Specification Proof Goals and Proof
52
242 Explicit Hardware Verification
53
243 ModelBased Proof Approaches
55
252 Variable Ordering Heuristics
71
26 Technical Details
76
261 Classes of Boolean Functions
77
27 Summary
80
Approaches Based on Finite State Machines
83
32 Formal Basics
84
321 Automata for Finite Sequences
85
322 Automata for Infinite Sequences
89
323 Image and PreImage of a Function
90
33 Modeling Hardware Behavior
93
34 Specification Proof Goal and Proof
94
341 Symbolic State Machine Traversal
95
35 Further Developments
100
351 Structural Approaches to Circuit Equivalence
102
42 Formal Basics
153
422 The Propositional Temporal Logics CTL CTL and LTL
156
423 Comparing CTL LTL and CTL
164
424 Proof Algorithms
167
425 Comparing Proof Complexity
180
43 Modeling Hardware Behavior
183
431 Describing Implementations with Temporal Structures
184
432 Describing Implementations by Temporal Logic Formulas
188
441 Creating Temporal Logic Specifications
189
45 Further Developments
192
46 Technical Details
194
47 Summary
204
HigherOrder Logics
207
52 Formal Basics
209
522 First Order Logic
210
523 HigherOrder Logic
213
53 Modeling Hardware Behavior
225
532 Modeling Structures
227
55 Performing Proofs
228
551 Methodology for Establishing Circuit Correctness
229
552 Abstraction Mechanisms
235
553 Verification of Generic Circuits
242
56 Technical Details
245
562 Modeling Hardware Behavior
247
563 Formalizing Abstraction Mechanisms
249
57 Summary
253
Mathematical Basics
255
Axioms and Rules for CTL
267
Axioms and Rules for Higher Order Logic
271
References
277
Index
291
Copyright

Other editions - View all

Common terms and phrases

Popular passages

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

Bibliographic information