# Introduction to Formal Hardware Verification

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

### Popular passages

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