  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.
