Kropf Introduction to Formal Hardware Verification

1999
ISBN: 978-3-662-03809-3
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 299 Seiten, eBook

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.

Zielgruppe

Graduate

Autoren/Hrsg.

Kropf, Thomas

Inhaltsverzeichnis

Introduction. Setting the Context; Circuit Design; Fighting Design Errors; Verification versus Validation; Hardware Verification; The Success of Formal Hardware Verification; Limitations of Formal Hardware Verification; The Pragmatic Approach: Recipes for Verifying Circuits; Summary; Structure of the Book; Literature.- Boolean Functions. Motivation; Representations for Boolean Functions; Modeling Hardware Behavior; Specification, Proof Goals and Proof; Further Developments and Tools; Technical Details; Summary.- Finite State Machine Based Approaches. Motivation; Formal Basics; Modeling Hardware Behavior; Specification, Proof Goal and Proof; Further Developments; Summary.- Propositional Temporal Logics. Motivation; Formal Basics; Modeling Hardware Behavior; Specification, Proof Goal and Proof; Further Developments; Technical Details; Summary.- Higher Order Logic. Motivation; Formal Basics; Modeling Hardware Behavior; Specification and Proof; Performing Proofs; Technical Details; Conclusion.- Appendix A: Mathematical Basics; Appendix B: Axioms and Rules for CTL*; Appendix C: Axioms and Rules for Higher Order Logic.- References.- Index