+612 9045 4394
Introduction to Formal Hardware Verification - Thomas Kropf

Introduction to Formal Hardware Verification

Hardcover Published: 16th October 1999
ISBN: 9783540654452
Number Of Pages: 299

Share This Book:


RRP $257.99
or 4 easy payments of $44.56 with Learn more
Ships in 7 to 10 business days

Other Available Editions (Hide)

  • Paperback View Product Published: 9th December 2010

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 and temporal logic model checking, and introduces the use of higher-order logic theorem proving for verifying circuit correctness. Each chapter contains an introduction and a summary as well as a section for the advanced reader, aiding an understanding of the advantages and limitations of each technique. Backed by many examples and illustrations, this text will appeal to a broad audience, from beginners in system design to experts. XXXXXXX Neuer Text This is a complete overview of existing techniques for hardware verification. It covers all approaches used in existing verification tools, such as symbolic methods for equivalence checking, temporal logic model checking, and higher-order logic theorem proving for verifying circuit correctness. The book helps readers to understand the advantages and limitations of each technique. Each chapter contains a summary as well as a section for the advanced reader.

Introductionp. 1
Setting the Contextp. 1
Faults and the Design Cyclep. 2
Avoiding Design Errors in Hardware Designsp. 3
Circuit Designp. 4
Fighting Design Errorsp. 8
Verification versus Validationp. 10
Hardware Verificationp. 10
Verification versus Simulationp. 11
Formal Specificationsp. 12
Formal Implementation Descriptionp. 15
Correctness Relation and Proofp. 18
The Success of Formal Hardware Verificationp. 21
Prerequisites for the Success of Hardware Verificationp. 22
Properties of Successful Hardware Verification Approachesp. 23
Limitations of Formal Hardware Verificationp. 25
The Pragmatic Approach - Recipes for Verifying Circuitsp. 26
Summaryp. 26
Structure of the Bookp. 28
Literaturep. 28
Boolean Functionsp. 31
Motivationp. 31
Hardware Verification Tasksp. 31
Representations for Boolean Functionsp. 32
Function Tablesp. 33
Propositional Logicp. 34
Binary Decision Diagramsp. 37
Modeling Hardware Behaviorp. 48
Functional Circuit Representationp. 48
Relational Circuit Representationp. 49
Characteristic Functionsp. 51
Specification, Proof Goals and Proofp. 52
Implicit Hardware Verificationp. 52
Explicit Hardware Verificationp. 53
Model-Based Proof Approachesp. 55
Further Developments and Toolsp. 55
Extensions and Variants of Binary Decision Diagramsp. 55
Variable Ordering Heuristicsp. 71
Technical Detailsp. 76
Classes of Boolean Functionsp. 77
Summaryp. 80
Approaches Based on Finite State Machinesp. 83
Motivationp. 83
Formal Basicsp. 84
Automata for Finite Sequencesp. 85
Automata for Infinite Sequencesp. 89
Image and Pre-Image of a Functionp. 90
Modeling Hardware Behaviorp. 93
Specification, Proof Goal and Proofp. 94
Symbolic State Machine Traversalp. 95
Further Developmentsp. 100
Structural Approaches to Circuit Equivalencep. 102
Relational FSM Representationp. 103
Functional FSM Representationp. 114
State Space Traversal Variantsp. 119
ROBDD Variable Ordering for FSM Equivalence Checkingp. 132
Verification of Sequential Circuits without Reset Linesp. 133
Verification based Test Generation for Fabrication Faultsp. 147
Summaryp. 148
Propositional Temporal Logicsp. 151
Motivationp. 151
Formal Basicsp. 153
Temporal Structuresp. 153
The Propositional Temporal Logics CTL*, CTL and LTLp. 156
Comparing CTL, LTL and CTL*p. 164
Proof Algorithmsp. 167
Comparing Proof Complexityp. 180
Modeling Hardware Behaviorp. 183
Describing Implementations with Temporal Structuresp. 184
Describing Implementations by Temporal Logic Formulasp. 188
Specification, Proof Goal and Proofp. 188
Creating Temporal Logic Specificationsp. 189
Further Developmentsp. 192
Increasing Efficiencyp. 192
Specificationsp. 192
Technical Detailsp. 194
Proof Algorithmp. 194
Summaryp. 204
Higher-Order Logicsp. 207
Motivationp. 207
Formal Basicsp. 209
Formal Systemsp. 209
First Order Logicp. 210
Higher-Order Logicp. 213
Modeling Hardware Behaviorp. 225
Representing Modules by Predicatesp. 225
Modeling Structuresp. 227
Specification and Proofp. 227
Performing Proofsp. 228
Methodology for Establishing Circuit Correctnessp. 229
Abstraction Mechanismsp. 235
Verification of Generic Circuitsp. 242
Technical Detailsp. 245
Some More Theoryp. 245
Modeling Hardware Behaviorp. 247
Formalizing Abstraction Mechanismsp. 249
Summaryp. 253
Mathematical Basicsp. 255
Axioms and Rules for CTL*p. 267
Axioms and Rules for Higher Order Logicp. 271
Referencesp. 277
Indexp. 291
Table of Contents provided by Publisher. All Rights Reserved.

ISBN: 9783540654452
ISBN-10: 3540654453
Audience: Professional
Format: Hardcover
Language: English
Number Of Pages: 299
Published: 16th October 1999
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.4 x 15.6  x 1.91
Weight (kg): 0.52