Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback

Peter-Michael Seidel
(Advanced Micro Devices)

We present the formal verification of a low-power x86 floating-point multiplier. The multiplier operates iteratively and feeds back intermediate results in redundant representation. It supports x87 and SSE instructions in various precisions and can block the issuing of new instructions. The design has been optimized for low-power operation and has not been constrained by the formal verification effort. Additional improvements for the implementation were identified through formal verification. The formal verification of the design also incorporates the implementation of clock-gating and control logic. The core of the verification effort was based on ACL2 theorem proving. Additionally, model checking has been used to verify some properties of the floating-point scheduler that are relevant for the correct operation of the unit.

In David Hardin and Julien Schmaltz: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2011), Austin, Texas, USA, November 3-4, 2011, Electronic Proceedings in Theoretical Computer Science 70, pp. 70–83.
Published: 20th October 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: