Digit Serial Methods with Applications to Division and Square Root (with mechanically checked correctness proofs)
This work provides a formal, verified framework for designing digit serial algorithms, which is incremental for the field of computer arithmetic.
The paper presents a generic digit serial method (DSM) for computing digits of a real number, with derived bounds on digits and errors, applied to high-radix division and square root algorithms. All claims are mechanically verified using the HOL-Light theorem prover.
We present a generic digit serial method (DSM) to compute the digits of a real number $V$ . Bounds on these digits, and on the errors in the associated estimates of $V$ formed from these digits, are derived. To illustrate our results, we derive such bounds for a parameterized family of high-radix algorithms for division and square root. These bounds enable a DSM designer to determine, for example, whether a given choice of parameters allows rapid formation and rounding of its approximation to $V$. All our claims are mechanically verified using the HOL-Light theorem prover, and are included in the appendix with commentary.