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.