Veri ation of Hardware ombining
Multipli ation, Division and Square RootColin D. Walter
Computation Department, U.M.I.S.T.,
PO Box 88, Sa kville Street, Man hester M60 1QD, U.K.
e-mail: dwsna. o.umist.a .uk

Index Terms: Computer arithmeti , multipli ation, division, square root, redundant number systems, re urren e relations.

Abstra tThis note provides a proof, orre tions and minor generalisation of algorithms
used by M. Er egova and T. Lang for implementing a hardware module thatombines multipli ation, division and square root. A onsequen e of the proofis the supply of initialisation onditions and bounds for register ontents. Some
subtleties required of an implementation are also noted.
1Introdu tion.

In [3℄ Er egova and Lang des ribe a hardware design whi h ombines algorithms
for multipli ation, division and square root and generates output digit serially.
The work des ribed here emanates from problems one of my proje t students hadin proving the orre tness of the design: without seeing a step-by-step derivationof the algorithm it was diÆ ult to know how to set about verifying it.
The same authors in [2℄ explain how \on-line" algorithms might be derived.
These are algorithms in whi h the inputs are onsumed and the outputs generated digit serially at the same rate, most signi ant bit rst. The te hniques in[2℄ are appli able in general for iterative arithmeti , in luding here, where mostinputs are provided entirely at initialisation, and the outputs produ ed one digit
at a time. However, at least for the square root, further ideas are ne essary toomplete the details of the proof.
Re ent advan es in te hnology have triggered mu h resear h into arithmeti
by enabling in reased speed to be gained at the ost of relatively heap hardware. The square root algorithm has, of ourse, been extensively studied. In
parti ular, a version of the algorithm here appears in [7℄, and ones using higher
bases appear in [4℄ and [8℄, where di erent initialisation omplexities arise. The
use of Newton-Raphson iteration for the square root is studied in [6℄. Although2C. D. Walter, Hardware Veri ation

it has quadrati rather than linear onvergen e so that it is apparently faster,
the method involves more arithmeti per iteration (a full length squaring) whi h
destroys any advantage.
On the ba k of the square root ase, at little further expense we have in luded
proofs for the multipli ation and division algorithms. This makes sense be ausesome initialisation detail is missing in [3℄ and indeed the former produ es ananswer whi h is out by a fa tor of 2. Combined modules for multipli ation,division and square root have also been studied in [10℄ where the radix is 4. The
multipli ation method used there produ es output digit serially starting as usualwith the least signi ant digit, but here it is in the opposite order, in order tomat h the output of the other two algorithms. This type of multipli ation has
already been dis ussed in [5℄, whilst division follows the normal paper and pen ilmethod.
We start with a derivation of some re urren e relations. This proves only thepartial orre tness of the algorithms. Total orre tness requires also a demonstration of onvergen e; more spe i ally, that run-time errors are not ausedby over ow. This se ond part of the proof reveals and exhibits some subtle detail of what is required from a hardware implementation, in luding bounds onregister ontents, and enables us to note some potential problems if the originaldes ription is varied in any way.
2Notation.

Sin e reals are generally expressed in sign/mantissa/exponent form, we will assume all mantissa representations are shifted to make the rst non-zero digit
orrespond to a negative power of the radix 2, normally to 2 1 . As al ulations
with the exponents and signs are relatively straight-forward here, only operations
on the mantissas are onsidered further.
We adopt notation in whi h upper ase hara ters are used to denote real
numbers and lower
ters to denote digits. So we onsider
repreP asem hara
Pj numberttsentations M = 1
2,andsequenessuhas
M [j ℄ =mt 2(j  0)
t
t=1
t=1
where mt is a digit. The latter arise for inputs and outputs whose digits are supplied or generated serially.
The addition of two numbers an lead to arbitrarily long arry propagation
if a standard non-redundant binary output is demanded. However, onsiderable
speedup is derived by allowing a redundant representation for the output sin earry propagation an then be limited, thus enabling digit operations to be
performed in parallel. The algorithms here use a representation for the outputsof an addition with digits in the range 0::2.
Speed is also a hieved by ignoring less signi ant digits. This leads to lesspre ision in the digits of the outputs of the algorithms. The inexa titude isMi ropro essors & Mi rosystems, vol. 19, 1995, pp. 243-245

3

re overed in subsequent digits by allowing a wider range of digits for the outputs,
namely 1::1. By in orporating an appropriate onstant delay into su h outputs,
it is possible to onvert to a di erent redundant representation, or generate two
onverging non-redundant representations whi h bra ket the value (see [1℄).
3

The Re urren e Relations.

The derivation of the re urren e relations of Er egova and Lang [3℄ is straightforward. The key step is to de ne a residual error or partial remainder W [j ℄ forthe j th iteration. This is a measure of the di eren e between the desired operation on the inputs so far and the output generated so far. It is de ned iteratively,
and at ea h iteration another output digit is hosen to approximately minimise
its next value. Convergen e of the output to the right answer is guaranteed
if this s aled residual error is bounded, and this in turn relies on appropriate
normalisation of the inputs and de nition of the output digits.
Following the notation of [3℄ we denote inputs by X and Y and outputs by(produ t), Q (quotient) and S (square root). The basi de nitions are mostonveniently written:

P

0 =X

Y

P

0 =XY



Q

0 =

2

X=(S S )=2

By taking approximations to about j pla es, they yield the expressions
2 j W [j ℄ = X Y [j +1℄ P [j ℄2 j W [j ℄ = X Y Q[j ℄2 j W [j ℄ = X=2 S [j ℄S [j ℄=2for j  0, whi h de ne W [j ℄ as the weighted residual error at the end of the j thiteration. Sin e the output digits have only positive indi es, the initial outputvalues satisfy
P [0℄= Q[0℄ = S [0℄ = 0In [3℄ it is assumed the inputs are in normalised non-redundant form, so that1 = 1=2 in the equation for multipli ation. Hen e the initial values
Y [1℄ = y1 2of W are respe tively:
W [0℄ = X=2W [0℄ = X
W [0℄ = X=2
The re urren e relations are obtained by using the formula M [j ℄ = M [j 1℄ + 2 j mj
applied to Y , P , Q and S in the relations for W [j ℄ and then subtra ting the expressions for W [j 1℄. Thus, for j  1,[ ℄ = 2W [j 1℄ + yj +1 X=2[ ℄ = 2W [j 1℄ qj YW [j ℄ = 2W [j1℄ sj S [j 1℄

W jpj

W j

2 j 1 sj 2

4

C. D. Walter, Hardware Veri ation

The quantities on the right side of these relations show what data must
be available as input to the iteration, and hen e most memory requirements
in an implementation. Hardware for implementing the algorithms needs tworegisters for redundant representations (W and one of X , Y or S ) plus a y li ally
rotatable binary register in whi h to store 2 j .
Comparing these algorithms with those des ribed in [3℄, the re urren e relations for division and square root agree, but not that for multipli ation: every
appearan e of X in the multipli ation algorithm here appears as X=2 in [3℄, sothat P = Y X=2 is al ulated there rather than the true produ t { even thebound of X < 1=2 here appears as the bound X < 1 there. So we must re ord
this as an error in [3℄, although the normalisation of the output there should automati ally orre t the unwanted fa tor of 2. The initialisation for W [0℄, whi his omitted from [3℄, is given above.
4Output Digits and Residual Error Bounds.

The output digits are hosen to minimise the next residual error as far as possibleusing a minimal amount of omputation. The redundant representation allows
some exibility in their hoi e so that an estimate W [j ℄0 of W [j ℄ is only neededto two pla es after the point. As W is the output from a arry save adder it hasdigits in the range 0::2. Consequently,[ ℄0W j

[ ℄W j<[ ℄0 + 1=2W j(1)Thus W [j ℄0 + 1=4 is, on average, the best approximation to W [j ℄. So Er egova

and Lang de ne:

8 1 if<=: 01 ifif

pj

==qj
sj

[ 1℄0  0W [j1℄0 < 1=4 orW [j1℄0  3=40
sign( W [j1℄ + 1=4 )sign( W [j1℄0 + 1=4 )W j

9=1 2;=

where sign maps onto the digit set f 1; 0; +1g in the obvious way. By hoosing
a more a urate approximation W 0 it is possible to in rease the number of zero
output digits so that the iterative step redu es from an addition to a simple left
shift, and performan e an then be improved (see [9℄).
Establishing the onvergen e of the algorithms requires hoosing exa tly theright bounds for the residual error. They are obtained by sele ting expressions
whi h will only just work in the proofs.
Theorem 1. If 0  X < 1=2, 1=2  Y < 1 and Y has the usual nonredundant binary representation then the residual error in the multipli ation algorithm is bounded by1

[ ℄W j<12X= 1for all j  0 :Mi ropro essors & Mi rosystems, vol. 19, 1995, pp. 243-245

5. If 0  X < 1=2 and 1=2  Y < 1 then the absolute value ofthe residual error in the division algorithm is bounded byTheorem 2j [ ℄j W j

Y

<1for all j  0 :. ( f (7) in [7℄.) If 1=4  X < 1 and either W [0℄ is in nonredundant binary form when s1 is omputed or s1 = 1 is for ed, theni) W [j ℄ 2 j 1 < S [j ℄ < 1for all j  0 ;ii) 1 <S [j ℄  W [j ℄2 j 1 for all j  1 .

Theorem 3

For the rst two theorems the ase of j = 0 follows dire tly from the initial
onditions. The rest follows easily by indu tion on j using (1) in a ase by ase
analysis of output digit values. For the square root algorithm the same line ofreasoning works providing that a suÆ iently good lower bound on S [j ℄ is known.
This is given by the lemma below, but rst note that the extra initialisation property is needed. Thus, if X = :01::: produ es the representation W [0℄ = 1:1122:::(= X=2) at the time s1 is al ulated, then s1 = 0 would result. Sin e su h X and2 ould not hold.
S would then satisfy X  1=4 and S < 1=2, the relation X = SHowever, if W [0℄ has standard binary form then s1 = 1 results. So for a orre talgorithm s1 = 1 must always hold independently of the representation of W [0℄and it may need to be for efully initialised.
We need to distinguish two ases: we all sj an initial zero of S if si = 0
whenever i satis es 1 < i  j and a non-initial zero of S if sj = 0 but si 6= 0 forsome i satisfying 1 < i < j .
. Given the initialisation of Theorem 3,i) If sj is an initial zero then S [j ℄ = S [1℄ = 1=2 ;ii) If sj is the rst non-zero digit with j > 1 then sj = 1 ;iii) If sj is a non-initial zero then S [j ℄ > 1=2 + 2 j 1 .

Lemma

Proof. Part (i) is immediate from s1 = 1. Now suppose si = 0 for 1 < i < j .
Then W [j 1℄ = 2j 2 (X 2 2 )  0. Hen e W [j 1℄0 > W [j 1℄ 1=2  1=2. So
sj 6=
1, giving part (ii). However, if sj is a non-initial zero and si 1 is the lastinitial zero then[ ℄S j[ 1℄ + 2 i (2 i 1 + ::: + 2 j +1 ) = 1=2 + 2 j +1

S i>

1=2 + 2 j 1:. With the initialisation given in the theorems and earlier, allthree algorithms onverge to the orre t answer, and jW [j ℄j  1 for allj  0.
CorollaryThis is lear, given S [j ℄  1 2 j . It is worth remarking that jW [j ℄j = 1
ould a tually arise, but only for multipli ation (for example, take X = 1=4 andY = 1=2 with j  3).

65C. D. Walter, Hardware Veri ation
Summary and Con lusions.

We have proved the total orre tness of the algorithms used in [3℄ subje t to aorre ting fa tor of 2 in the ase of multipli ation, and a guarantee that s1 = 1
in the ase of the square root. The re urren e relations for them were derived
in x3, where the initial onditions, omitted from [3℄, are lari ed. The de nitionof the output digits is given at the start of x4. The inputs are subje t to therange and representation restri tions stated in the theorems. As these are lessdemanding than those in [3℄ the theorems have been slightly generalised. The
serially produ ed output is always within 1 in the most re ent digit position of
being the orre t in nite pre ision answer. Finally, in all ases, the residual error
W [j ℄ has absolute value at most 1 and so hardware registers of the right size an
now be supplied.
Referen es[1℄ Milos D. Er egova & Tomas Lang, \On-the- y onversion of redundant into onventional representations", IEEE Trans. Comput., vol. C-36, pp. 895-897, July1987.
[2℄ Milos D. Er egova & Tomas Lang, \On-Line Arithmeti : A Design Methodology
and Appli ations in Digital Signal Pro essing", VLSI Signal Pro essing III, R. W.
Brodersen, H. S. Mos ovitz eds., pp. 252-263, IEEE Press, New York, 1988.
[3℄ Milos D. Er egova & Tomas Lang, \Implementation of a Module ombining Multipli ation, Division and Square Root", Pro . IEEE Intern. Symp. on Cir uits andSystems, 1989, pp. 150-153.
[4℄ Milos D. Er egova & Tomas Lang, \Radix-4 Square Root Without Initial PLA",IEEE Trans. Comput., vol. C-39, pp. 1016-1024, August 1990.
[5℄ Milos D. Er egova & Tomas Lang, \Fast Multipli ation Without Carry-Propagate
Addition", IEEE Trans. Comput., vol. C-39, pp. 1385-1390, November, 1990.
[6℄ Reza Hashemian, \Square Root Algorithms for Integer and Floating point Numbers", IEEE Trans. Comput., vol. C-39, pp. 1025-1029, August 1990.
[7℄ Stanislaw Majerski, \Square Rooting Algorithms for High Speed Digital Cir uits",
IEEE Trans. Comput., vol. C-34, pp. 724-733, August 1985.
[8℄ Paolo Montus hi & Luigi Ciminiera, \On the eÆ ient implementation of higher
radix square root algorithms", Pro . 9th IEEE Symposium on Computer Arithmeti , Santa Moni a, CA, pp. 154-161, 1989.
[9℄ Paolo Montus hi & Luigi Ciminiera, \Redu ing Iteration Time When Result Digitis Zero for Radix 2 SRT Division and Square Root with Redundant Remainders",
IEEE Trans. Comput., vol. 42, pp. 239-246, February 1993.
[10℄ J. H. Zurawski & J. B. Gosling, \Design of a high-speed square root, multiply anddivide unit", IEEE Trans. Comput., vol. C-36, pp. 13-23, 1987.