Divider circuit verification with model checking and theorem proving

DOI10.1007/3-540-44659-1_21MaRDI QIDQ2754053zbMATH OpenFDO

Authors Roope Kaivola, Mark D. Aagaard

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44659-1_21

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Proof engineering in the large: Formal verification of Pentium^ 4 floating-point divider
• A light-weight framework for hardware verification
• Formal modeling and verification of microprocessors
• Verification: industrial applications
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor

Cited in

(7)

• Proof engineering in the large: Formal verification of Pentium^ 4 floating-point divider
• Deciding floating-point logic with abstract conflict driven clause learning
• Verification: industrial applications
• A light-weight framework for hardware verification
• Efficient and accurate computation of upper bounds of approximation errors
• Formal verification of the VAMP floating point unit
• Formalization of fixed-point arithmetic in HOL

This page was built for publication: Divider circuit verification with model checking and theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2754053)