| Introduction | p. 1 |
| Setting the Context | p. 1 |
| Faults and the Design Cycle | p. 2 |
| Avoiding Design Errors in Hardware Designs | p. 3 |
| Circuit Design | p. 4 |
| Fighting Design Errors | p. 8 |
| Verification versus Validation | p. 10 |
| Hardware Verification | p. 10 |
| Verification versus Simulation | p. 11 |
| Formal Specifications | p. 12 |
| Formal Implementation Description | p. 15 |
| Correctness Relation and Proof | p. 18 |
| The Success of Formal Hardware Verification | p. 21 |
| Prerequisites for the Success of Hardware Verification | p. 22 |
| Properties of Successful Hardware Verification Approaches | p. 23 |
| Limitations of Formal Hardware Verification | p. 25 |
| The Pragmatic Approach - Recipes for Verifying Circuits | p. 26 |
| Summary | p. 26 |
| Structure of the Book | p. 28 |
| Literature | p. 28 |
| Boolean Functions | p. 31 |
| Motivation | p. 31 |
| Hardware Verification Tasks | p. 31 |
| Representations for Boolean Functions | p. 32 |
| Function Tables | p. 33 |
| Propositional Logic | p. 34 |
| Binary Decision Diagrams | p. 37 |
| Modeling Hardware Behavior | p. 48 |
| Functional Circuit Representation | p. 48 |
| Relational Circuit Representation | p. 49 |
| Characteristic Functions | p. 51 |
| Specification, Proof Goals and Proof | p. 52 |
| Implicit Hardware Verification | p. 52 |
| Explicit Hardware Verification | p. 53 |
| Model-Based Proof Approaches | p. 55 |
| Further Developments and Tools | p. 55 |
| Extensions and Variants of Binary Decision Diagrams | p. 55 |
| Variable Ordering Heuristics | p. 71 |
| Technical Details | p. 76 |
| Classes of Boolean Functions | p. 77 |
| Summary | p. 80 |
| Approaches Based on Finite State Machines | p. 83 |
| Motivation | p. 83 |
| Formal Basics | p. 84 |
| Automata for Finite Sequences | p. 85 |
| Automata for Infinite Sequences | p. 89 |
| Image and Pre-Image of a Function | p. 90 |
| Modeling Hardware Behavior | p. 93 |
| Specification, Proof Goal and Proof | p. 94 |
| Symbolic State Machine Traversal | p. 95 |
| Further Developments | p. 100 |
| Structural Approaches to Circuit Equivalence | p. 102 |
| Relational FSM Representation | p. 103 |
| Functional FSM Representation | p. 114 |
| State Space Traversal Variants | p. 119 |
| ROBDD Variable Ordering for FSM Equivalence Checking | p. 132 |
| Verification of Sequential Circuits without Reset Lines | p. 133 |
| Verification based Test Generation for Fabrication Faults | p. 147 |
| Summary | p. 148 |
| Propositional Temporal Logics | p. 151 |
| Motivation | p. 151 |
| Formal Basics | p. 153 |
| Temporal Structures | p. 153 |
| The Propositional Temporal Logics CTL*, CTL and LTL | p. 156 |
| Comparing CTL, LTL and CTL* | p. 164 |
| Proof Algorithms | p. 167 |
| Comparing Proof Complexity | p. 180 |
| Modeling Hardware Behavior | p. 183 |
| Describing Implementations with Temporal Structures | p. 184 |
| Describing Implementations by Temporal Logic Formulas | p. 188 |
| Specification, Proof Goal and Proof | p. 188 |
| Creating Temporal Logic Specifications | p. 189 |
| Further Developments | p. 192 |
| Increasing Efficiency | p. 192 |
| Specifications | p. 192 |
| Technical Details | p. 194 |
| Proof Algorithm | p. 194 |
| Summary | p. 204 |
| Higher-Order Logics | p. 207 |
| Motivation | p. 207 |
| Formal Basics | p. 209 |
| Formal Systems | p. 209 |
| First Order Logic | p. 210 |
| Higher-Order Logic | p. 213 |
| Modeling Hardware Behavior | p. 225 |
| Representing Modules by Predicates | p. 225 |
| Modeling Structures | p. 227 |
| Specification and Proof | p. 227 |
| Performing Proofs | p. 228 |
| Methodology for Establishing Circuit Correctness | p. 229 |
| Abstraction Mechanisms | p. 235 |
| Verification of Generic Circuits | p. 242 |
| Technical Details | p. 245 |
| Some More Theory | p. 245 |
| Modeling Hardware Behavior | p. 247 |
| Formalizing Abstraction Mechanisms | p. 249 |
| Summary | p. 253 |
| Mathematical Basics | p. 255 |
| Axioms and Rules for CTL* | p. 267 |
| Axioms and Rules for Higher Order Logic | p. 271 |
| References | p. 277 |
| Index | p. 291 |
| Table of Contents provided by Publisher. All Rights Reserved. |
