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 . Index Terms-Digit serial method, digit recurrence method, mixed-radix representation, on-the-fly technique, high-radix, division, square root, digit bounds, error bounds Ç LET V be a real number. A digit serial method (DSM) is an algorithm that determines the digits of V serially, starting with the leading digit. A DSM begins by initializing an accumulator to zero and, as each digit is determined, that digit is aligned and added to the accumulator. Successive values of this accumulator form a sequence of estimates of V . The primary contribution of this paper is a generic DSM analysis method for determining bounds on the magnitudes of the digits, as well as bounds on the error associated with the estimates of V . These bounds allow a designer to determine the required bitwidth of signals representing these digits and errors, and to determine when the estimates of V can be efficiently formed and rounded by, say, on-the-fly techniques. The major results presented here are the Proxy Theorem 5.1 and its Corollary 5.3 with illustrations of their application to division and square root algorithms. These results have been checked/formalized using the HOL Light [1] theorem prover; a short extract from the formalization is presented in Section 10. The analysis of low-radix DSM for division and square root is well-understood [2]. Analyses of specific high-radix DSM for these operations are described in [3] , [4], [5] . An additional contribution of this paper is the application of our generic DSM analysis to a parameterized family of high-radix DSM algorithms for division and square root. W. Ferguson is retired from Intel Corporation, Hillsboro, OR 97124.
In 2018, Intel Corporation presented a research paper about the proof of correctness of square root using a digit serial method (DSM) and a theorem prover (HOL-Light) REF .
Digit Serial Methods with Applications to Division and Square Root
IEEE Transactions on Computers
IEEE Transactions on Computers
Computer Science Mathematics