In this section, we explore the gate-level implementation of bit vector addition. Our objective is the computation of the -bit sum of n-bit vectors and . As a first step, we consider the simple 2-gate module of Figure 11.1, known a half adder. According to the first lemma below, the outputs of this module may be interpreted as the sum of its inputs.

PROOF: The equation may be checked exhaustively, i.e., for all 4 possible combinations of and

The propagate and generate bits of two -bit summands and are defined as

and

respectively, for . Obviously, the vectors and may be computed by a circuit consisting of half adders, as shown in the figure below. The following lemma gives a reformulation of in terms of and .

(add2) Given and -bit vectors and , let and . Then

-

PROOF: By Lemmas 2.2.5 and 2.3.17,

 --

Appealing to induction, we may assume that

------

which reduces, by Lemma 3.1.13, to --. By Lemma 11.1.1,
 -- ---- -- --

Thus, by Lemma 2.3.17,
 -- -

In order to represent as a single vector, we shall require a more complex module, known as a full adder, composed of two half adders and an or-gate, as shown in the figure below. The outputs of the full adder may be readily computed as

and

Its arithmetic functionality is characterized as follows.

(full-adder) If , , and are 1-bit vectors, then

PROOF: The equation may be checked exhaustively, i.e., for all 8 possible combinations of , , and

Thus, a full adder computes the 2-bit sum of three 1-bit inputs. Replacing the half adders of Figure 11.2 with full adders results in the 3:2 compressor shown in the figure below, which reduces a sum of three vectors to a sum of two.

(add3) Given and -bit vectors , , and , let

and

Then

PROOF: By Lemmas 2.2.5 and 2.3.17,

 ---

By induction, we may assume that

-----

and by Lemma 11.1.3,
 ------ ---

By Lemma 3.1.14,

----

and by Lemmas 3.1.14 and 2.3.15,

-------

Thus, invoking Lemma 2.3.17, we have
 -

The module displayed above is constructed from the same hardware as the 3:2 compressor, but the third input of each adder is elimated, replaced by , the carry bit generated at index . The resulting circuit, known as a ripple-carry adder, produces the sum of the two input vectors, .

(ripple-carry) Given , , and , let and such that and for ,

and

Then

---

PROOF: We shall show, by induction on , that for ,

----

The claim is trivial for ; assume that it holds for some , . Then by Lemmas 2.3.17 and 11.1.3,
 -- - -

Note that the execution time of the ripple-carry adder is a linear function of the width of the input vectors, since the carry bit is required for the computation of and . In order to improve the efficiency of bit vector addition, some degree of parallelism must be introduced in the computation of the carry bits. Our analysis of this problem is based on the functions prop and gen, which determine whether a carry is generated or propagated across a bit slice.

Definition 11.1.1   (gen) For all , , , and ,

Definition 11.1.2   (prop) For all , , , and ,

The value of determines whether the sum generates a carry out to bit . In particular, according to the following lemma, the carry bit of Lemma 11.1.5 is given by

PROOF: By Lemma 2.3.17,

-

and

-

Thus, if , then and

whereas if , then and by Lemma 2.2.1,

--

For the case , we have

We proceed by induction on , assuming that

---

Suppose that -. Then and

--

On the other hand, if -, then and

--

Lemma 11.1.6 may be restated as follows.

PROOF: By Lemma 2.2.1,

Therefore, by Lemmas 2.3.9 and 2.3.23,

In the case , we have the following equivalent formulation.

PROOF: By Lemma 2.2.1,

Thus, by Lemmas 2.2.5 and 2.3.17,

But by Corollary 11.1.7,

and by Lemma 2.2.9,

PROOF: If , then and by Lemmas 2.3.17 and 2.2.1,

which implies .

Conversely, suppose that , so that

Then , for otherwise we would have

which, according to Lemma 2.3.23, would contradict the assumption that

-

If , then indicates whether a carry into bit will be propagated out to bit :

(prop-val) For all , , , and , if , then

PROOF: By Lemmas 2.3.17 and 2.2.1,

-

and

-

where - and -. Through a simple case analysis, we conclude that

and --

Thus, if , then and according to Definition 11.1.2, . Now suppose that . Then by induction,
 -- -

PROOF: We shall show that

The claim is trivial for . Suppose .

By Lemmas 3.1.13, and 2.2.23,

and

Similarly, by Lemmas 3.1.14, and 2.3.16,

Thus, by Lemma 2.3.17,

But since

it follows that if and only if

and

i.e.,

and

Therefore, by induction,

and

But as noted in the proof of Lemma 11.1.10,

and --

The computation of gen and prop may be facilitated by decomposing the interval into subintervals.

(gen-extend) For all , , , , and , if , then

PROOF: First suppose . By Definition 11.1.1, and , and each side of the equation reduces to .

Next, suppose . By Definition 11.1.1, and By Definition 11.1.2, , and each side of the equation reduces to 0.

Thus, we may assume that . By expanding the definitions, we reduce the equation to

--+1-+

If , then

-+1-+1

and the right-hand side further reduces to

-

In the remaining case, the proof is completed by induction.

PROOF: Since

it follows from Lemmas 2.3.9 and 2.3.23 that

if and only if

But this inequality holds if and only if either

or

Applying Lemmas 11.1.6 and 11.1.10, we may write this disjunction as

which, according to Lemma 11.1.12, reduces to

(prop-extend) For all , , , , and , if , then

PROOF: If , then . Thus, we may assume . In this case, the equation reduces to

If , then -. In the remaining case, the proof is completed by induction.

Note that the propagate and generate bits that were defined in connection with Lemma 11.1.2 may be expressed as

and

By repeated applications of the above lemmas, prop and gen may computed as logical combinations of these bits: by Lemma 11.1.14,

and by Lemma 11.1.12,

This last equation is the basis for the design of a circuit called a carry-look-ahead adder, which computes the sum of two -bit vectors in constant time, independent of . In fact, this may be achieved in as few as four gate delays:

1. 1 gate delay to compute the generate and propagate bits,

and

2. 2 gate delays to compute the carry bits

using the above equation, and

3. 1 gate delay to compute the sum using the formula

However, this design is impractical for all but very small values of , since the number of gates required increases quadratically with and the gate fan-in increases linearly. In practice, carry-look-ahead adders are used only to compute the sums of narrow slices, , of summands and . The remaining results of this section pertain to the process of combining such segments to form the final sum .

PROOF: By Lemma 2.3.17 and Corollary 11.1.8,

 -- --

By Lemma 2.2.1, -, and hence

-

Now by Lemmas 2.2.23, 2.2.9, and 2.2.16,
 -

The next result deals with a special case in which the contribution of one of the summands may be ignored.

(bits-sum-swallow) Let , , , , and . If , , and , then

PROOF: Since , Lemmas 2.2.5 and 2.2.22 imply

+

and hence +. Since ,

-

by Lemmas 2.3.17 and 2.2.1. Hence,

and

+

By Lemmas 11.1.15 and 2.2.23,
 + ++-- +-- +

Finally, by Lemma 2.2.23,
 +---- +----

Here is a case in which a slice of the sum may be computed independently.

PROOF: By Lemma 11.1.15,

-

But by Lemma 11.1.6, and hence by Lemma 2.2.5,

-

The following lemma is an extension of Lemma 11.1.15 to handle three summands.

PROOF: Applying Lemma 11.1.15 twice and appealing to Corollary 2.2.9, we have

 - - -- --

The case is of particular interest.

PROOF: By Lemma 11.1.18, it suffices to show that

----

Suppose first that -. By Lemma 2.2.1,

--

Thus, by Lemma 2.2.5, Lemma 2.3.17, Corollary 11.1.7, and Corollary 2.2.9,
 -- -- ----- -- -

and hence -. It follows that -, and both sides of our equation reduce to 1.

Now suppose that -. In this case, we must show that

--

By Lemma 11.1.6,

--

and hence, by Corollary 2.2.9 and Lemma 2.2.5,

------

Now
 - -- -- -- - -

When the result of a sum is to be rounded, it is sometimes possible to arrange for one of the summands to contain a “hole” where the rounding constant may be inserted. In this case, we have three vectors to be added, two of which are known not to have any corresponding asserted bits. The following lemmas deal with this case.

PROOF: The proof is by induction on . The case is trivial. For , by Lemma 11.1.12,

We shall show that .

By Lemmas 2.3.16, 3.1.14, and 2.3.5,

 -- - -

It follows that either or . In either case, by Definition 11.1.1,

Similarly, by Lemmas 2.2.23, 3.1.14, and 2.2.15,
 -- ---- -- --

By induction, therefore,

PROOF: We may assume . By Lemmas 2.2.23, 3.1.14, and 2.2.15,

 -- -- - -

Thus, by Lemma 11.1.15,

-

Similarly,

and by Lemmas 11.1.20 and 11.1.6. Thus, by Lemma 2.2.5,

-

(gen-plus) Let , , , and . If , , and , then .

PROOF: By Corollary 11.1.8,

Thus, by Corollary 11.1.21 and Lemma 2.2.1,

The follows from Lemma 11.1.6

(gen-extend-3) Let , , , and with . Let be a -bit vector such that

Then

PROOF: Since , it is clear from Lemma 11.1.6 that

Thus, by Lemma 11.1.12,

We need only show that if gen(x+y, z, j, 0) = 1, then

By Lemma 11.1.22, , and by Lemma 11.1.15,
 -- --

Thus, by Lemma 11.1.10,
 --

whereas

It remains to show that

--

Suppose first that

--

By Lemma 2.2.1,

Therefore, by Lemmas 2.2.5 and 2.3.17,
 -

But by Lemma 2.2.1,

which implies -, and hence

On the other hand, if

then

--

by Lemma 2.2.5

David Russinoff 2017-08-01