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 7.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.

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

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.12, to -- . By Lemma 7.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 7.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 7.1.3,
 ------ ---

By Lemma 3.1.13,

----

and by Lemmas 3.1.13 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 7.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 7.1.1   (gen) For all , , , and ,

Definition 7.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 7.1.5 is given by

(gen-val) For all , , , and ,

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 7.1.6 may be restated as follows.

(gen-val-cor1) For all , , , and ,

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.

(gen-val-cor2) For all , , and ,

PROOF: By Lemma 2.2.1,

Thus, by Lemmas 2.2.5 and 2.3.17,

But by Corollary 7.1.7,

and by Lemma 2.2.9,

(gen-special-case) For all , , , and , if and

-

then

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 7.1.2, . Now suppose that . Then by induction,
 -- -

(prop-as-lxor) For all , , , and , if , then

PROOF: We shall show that

The claim is trivial for . Suppose .

By Lemmas 3.1.12, and 2.2.23,

and

Similarly, by Lemmas 3.1.13, 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 7.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 7.1.1, and , and each side of the equation reduces to .

Next, suppose . By Definition 7.1.1, and By Definition 7.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.

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

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 7.1.6 and 7.1.10, we may write this disjunction as

which, according to Lemma 7.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 7.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 7.1.14,

and by Lemma 7.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 .

(bits-sum) For all , , , and ,

-

PROOF: By Lemma 2.3.17 and Corollary 7.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 7.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.

(bits-sum-cor) For all , , , and , if

-

then

PROOF: By Lemma 7.1.15,

-

But by Lemma 7.1.6, and hence by Lemma 2.2.5,

-

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

(bits-sum-3) For all , , , , and ,
 --

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

 - - -- --

The case is of particular interest.

(bits-sum-plus-1) For all , , , , and ,

--

PROOF: By Lemma 7.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 7.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 7.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.

(logand-gen-0) For all , , , and , if

then

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

We shall show that .

By Lemmas 2.3.16, 3.1.13, and 2.3.5,

 -- - -

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

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

By induction, therefore,

(logand-gen-0-cor) For all , , , and , if

then

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

 -- -- - -

Thus, by Lemma 7.1.15,

-

Similarly,

and by Lemmas 7.1.20 and 7.1.6. Thus, by Lemma 2.2.5,

-

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

PROOF: By Corollary 7.1.8,

Thus, by Corollary 7.1.21 and Lemma 2.2.1,

The follows from Lemma 7.1.6

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

Then

PROOF: Since , it is clear from Lemma 7.1.6 that

Thus, by Lemma 7.1.12,

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

By Lemma 7.1.22, , and by Lemma 7.1.15,
 -- --

Thus, by Lemma 7.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