Computer Science – Logic in Computer Science
Scientific paper
2011-10-21
EPTCS 70, 2011, pp. 70-83
Computer Science
Logic in Computer Science
In Proceedings ACL2 2011, arXiv:1110.4473
Scientific paper
10.4204/EPTCS.70.6
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.
No associations
LandOfFree
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-84694