Introduction to Formal Hardware VerificationHardware 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. |
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 |
281 | |
295 | |
Other editions - View all
Common terms and phrases
abstraction level according to Def algorithm applied approaches automata automated axioms becomes true behavior Binary Decision Diagrams bit vectors Boolean functions characteristic function cofactor combinational circuits complete construction contain corresponding CTL model checking defined Definition denotes efficient elements equivalence checking Example existential quantification exists F T F fairness constraints faults finite state machines formal specification formal verification function f function tables function value gate given graph hardware verification Hence higher-order logic holds implementation input sequence input values iteration LTL formula modules natural numbers nodes OFDD order logic output function pairs path formula possible predicates product automaton proof goal properties propositional logic propositional temporal logics reachable recursive representation represented reset sequence ROBDD rules Sat(Q satisfiability semantics sequential circuits shown subset successor tableau techniques temporal logic temporal operators temporal structures Theorem tion transition relation traversal valuations variable ordering variants
Popular passages
Page 282 - Ma, and AR Newton. On the verification of sequential machines at differing levels of abstraction.