Introduction to formal hardware verification /
Kropf, Thomas, 1961-,
Introduction to formal hardware verification / Thomas Kropf. - ix, 299 pages : illustrations ; 25 cm
Includes bibliographical references (pages [277]-289) and index.
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
3540654453 (acidfree paper)
99012500
Integrated circuits--Very large scale integration--Computer-aided design.
Integrated circuits--Verification.
621.395 / K.T.I.
Introduction to formal hardware verification / Thomas Kropf. - ix, 299 pages : illustrations ; 25 cm
Includes bibliographical references (pages [277]-289) and index.
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
3540654453 (acidfree paper)
99012500
Integrated circuits--Very large scale integration--Computer-aided design.
Integrated circuits--Verification.
621.395 / K.T.I.