About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
Formal Methods in System Design
Paper
Introduction to the special issue on verification of arithmetic hardware
Abstract
Theorem proving techniques were verified as effective methods for the study of arithmetic hardware in commercial microprocessors. An introduction is given of the papers chosen as representative of theorem proving techniques. The subjects covered include SRT division algorithm, a theorem prover called Analytica, the PVS theorem, and the development of a correctness proof for the microprogram that performs the floating point square root operation in the AMD K5 processor.