next up previous contents
Next: Leading One Prediction Up: Addition Previous: Addition   Contents

Bit Vector Addition

In this section, we explore the gate-level implementation of bit vector addition. Our objective is the computation of the $ (n+1)$ -bit sum $ s = x+y$ of n-bit vectors $ x$ and $ y$ . As a first step, we consider the simple 2-gate module of Figure 6.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 $ u$ and $ v$ are 1-bit vectors, then

$\displaystyle u+v = \{u \;\verb!&!\; v, u \;\verb!^!\; v\}.$

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


Figure 6.1: Half Adder
\begin{figure}\par\setlength{\unitlength}{2mm} \begin{picture}(40,40)(-19,-8)... ...\put(3.5,29){\Large$u$} \put(19.5,29){\Large$v$} \end{picture}\par\end{figure}

The propagate and generate bits of two $ n$ -bit summands $ x$ and $ y$ are defined as

$\displaystyle p[k] = x[k] \;\verb!^!\; y[k]$

and

$\displaystyle g[k] = x[k] \;\verb!&!\; y[k],$

respectively, for $ k = 0,\ldots,n-1$ . Obviously, the vectors $ p$ and $ g$ may be computed by a circuit consisting of $ n$ half adders, as shown in the figure below. The following lemma gives a reformulation of $ x+y$ in terms of $ p$ and $ g$ .

  (add2) Given $ n \in \mathbb{N}$ and $ n$ -bit vectors $ x$ and $ y$ , let

$\displaystyle p = x[n$-$\displaystyle 1:0] \;\verb!^!\; y[n$-$\displaystyle 1:0]$

and

$\displaystyle g = x[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0].$

Then

$\displaystyle x+y = p + \{g[n$-$\displaystyle 1:0],1\verb!'b!0\}.$

PROOF: By Lemmas 2.2.11 and 2.3.13,

$\displaystyle x+y$ $\displaystyle =$ $\displaystyle x[n$-$\displaystyle 1:0] + y[n$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 2^{n\mbox{-}1}(x[n\mbox{-}1] + y[n\mbox{-}1]) + x[n\mbox{-}2:0] + y[n\mbox{-}2:0].$  

Appealing to induction, we may assume that

$\displaystyle x[n$-$\displaystyle 2:0] + y[n$-$\displaystyle 2:0] = x[n$-$\displaystyle 2:0] \;\verb!^!\; y[n$-$\displaystyle 2 :0] + 2(x[n$-$\displaystyle 2:0] \;\verb!&!\; y[n$-$\displaystyle 2:0]),$

which reduces, by Lemma 3.2.9, to $ p[n$-$ 2:0] + 2g[n$-$ 2:0]$ . By Lemma 6.1.1,
$\displaystyle x[n$-$\displaystyle 1] + y[n$-$\displaystyle 1]$ $\displaystyle =$ $\displaystyle \{x[n$-$\displaystyle 1] \;\verb!&!\; y[n$-$\displaystyle 1], x[n$-$\displaystyle 1] \;\verb!^!\; y[n$-$\displaystyle 1]\}$  
  $\displaystyle =$ $\displaystyle \{g[n$-$\displaystyle 1],p[n$-$\displaystyle 1]\}$  
  $\displaystyle =$ $\displaystyle 2g[n$-$\displaystyle 1] + p[n$-$\displaystyle 1].$  

Thus, by Lemma 2.3.13,
$\displaystyle x+y$ $\displaystyle =$ $\displaystyle 2^{n\mbox{-}1}(2g[n\mbox{-}1] + p[n\mbox{-}1]) + p[n\mbox{-}2:0] + 2g[n\mbox{-}2:0]$  
  $\displaystyle =$ $\displaystyle 2(2^{n\mbox{-}1}g[n\mbox{-}1] + g[n\mbox{-}2:0]) + (2^{n\mbox{-}1}p[n\mbox{-}1] + p[n\mbox{-}2:0])$  
  $\displaystyle =$ $\displaystyle 2g[n$-$\displaystyle 1:0] + p[n$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle p + \{g[n$-$\displaystyle 1:0],1\verb!'b!0\}.$  

Figure 6.2: Propagate and Generate Vectors
\begin{figure}\par\setlength{\unitlength}{2mm} \begin{picture}(64,24)(0,-8) \... ...} \put(52,-2){\large$g[0]$} \put(56,-5){\large$p[0]$} \end{picture} \end{figure}

In order to represent $ x+y$ 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

$\displaystyle u \;\verb!^!\; v \;\verb!^!\; w$

and

$\displaystyle u \;\verb!&!\; v \;\verb!\vert!\; (u \;\verb!^!\; v) \;\verb!&!\;... ...erb!&!\; v \;\verb!\vert!\; u \;\verb!&!\; w \;\verb!\vert!\; v \;\verb!&!\; w.$

Its arithmetic functionality is characterized as follows.

  (full-adder) If $ u$ , $ v$ , and $ w$ are 1-bit vectors, then

$\displaystyle u+v+w = \{u \;\verb!&!\; v \;\verb!\vert!\; u \;\verb!&!\; w \;\verb!\vert!\; v \;\verb!&!\; w,u \;\verb!^!\; v \;\verb!^!\; w\}.$

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


Figure 6.3: Full Adder
\begin{figure}\par\setlength{\unitlength}{2mm} \begin{picture}(40,40)(-19,-8)... ... \put(8,15.5){\large HA} \put(16,5.5){\large HA} \end{picture}\par\end{figure}

Thus, a full adder computes the 2-bit sum of three 1-bit inputs. Replacing the half adders of Figure 6.1 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.

Figure 6.4: 3:2 Compressor
\begin{figure} \setlength{\unitlength}{2mm} \begin{picture}(64,35)(0,-8) \put(5... ...} \put(35.5,4.5){\Large FA} \put(52.5,4.5){\Large FA} \end{picture} \end{figure}

  (add3) Given $ n \in \mathbb{N}$ and $ n$ -bit vectors $ x$ , $ y$ , and $ z$ , let

$\displaystyle a = x[n$-$\displaystyle 1:0] \;\verb!^!\; y[n$-$\displaystyle 1:0] \;\verb!^!\; z[n$-$\displaystyle 1:0]$

and

$\displaystyle b = \{x[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0] \;\verb!\vert!\; x[n$-$\displaystyle 1:0] \;\verb!&!\; z[n$-$\displaystyle 1:0] \;\verb!\vert!\; y[n$-$\displaystyle 1:0] \;\verb!&!\; z[n$-$\displaystyle 1:0],1\verb!'b!0\}.$

Then

$\displaystyle x + y + z = a + b.$

PROOF: By Lemmas 2.2.11 and 2.3.13,

$\displaystyle {x+y+z}$
  $\displaystyle =$ $\displaystyle x[n$-$\displaystyle 1:0] + y[n$-$\displaystyle 1:0] + z[n$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 2^{n\mbox{-}1}(x[n\mbox{-}1] + y[n\mbox{-}1] + z[n\mbox{-}1]) + x[n\mbox{-}2:0] + y[n\mbox{-}2:0] + z[n\mbox{-}2:0].$  

By induction, we may assume that

$\displaystyle x[n$-$\displaystyle 2:0] + y[n$-$\displaystyle 2:0] + z[n$-$\displaystyle 2:0] = a[n$-$\displaystyle 2:0] + b[n$-$\displaystyle 1:0],$

and by Lemma 6.1.3,
$\displaystyle {x[n\mbox{-}1] + y[n\mbox{-}1] + z[n\mbox{-}1]}$
  $\displaystyle =$ $\displaystyle 2(x[n$-$\displaystyle 1] \;\verb!&!\; y[n$-$\displaystyle 1] \;\verb!\vert!\; x[n$-$\displaystyle 1] \;\verb!&!\; z[n$-$\displaystyle 1] \;\verb!\vert!\; y[n$-$\displaystyle 1] \;\verb!&!\; z[n$-$\displaystyle 1])$  
    $\displaystyle + x[n$-$\displaystyle 1] \;\verb!^!\; y[n$-$\displaystyle 1] \;\verb!^!\; z[n$-$\displaystyle 1].$  

By Lemma 3.2.10,

$\displaystyle x[n$-$\displaystyle 1] \;\verb!^!\; y[n$-$\displaystyle 1] \;\verb!^!\; z[n$-$\displaystyle 1] = a[n$-$\displaystyle 1]$

and by Lemmas 3.2.10 and 2.3.11,

$\displaystyle x[n$-$\displaystyle 1] \;\verb!&!\; y[n$-$\displaystyle 1] \;\verb!\vert!\; x[n$-$\displaystyle 1] \;\verb!&!\; z[n$-$\displaystyle 1] \;\verb!\vert!\; y[n$-$\displaystyle 1] \;\verb!&!\; z[n$-$\displaystyle 1] = \lfloor b/2 \rfloor[n$-$\displaystyle 1]= b[n].$

Thus, invoking Lemma 2.3.13, we have
$\displaystyle x+y+z$ $\displaystyle =$ $\displaystyle 2^{n\mbox{-}1}(2b[n] + a[n\mbox{-}1]) + a[n\mbox{-}2:0] + b[n\mbox{-}1:0]$  
  $\displaystyle =$ $\displaystyle (2^{n\mbox{-}1}a[n\mbox{-}1] + a[n\mbox{-}2:0]) + (2^nb[n] + b[n\mbox{-}1:0])$  
  $\displaystyle =$ $\displaystyle a[n$-$\displaystyle 1:0] + b[n:0]$  
  $\displaystyle =$ $\displaystyle a + b.$  

Figure 6.5: Ripple-Carry Adder
\begin{figure} \setlength{\unitlength}{2mm} \begin{picture}(64,35)(0,-8) \put(5... ...} \put(35.5,4.5){\Large FA} \put(52.5,4.5){\Large FA} \end{picture} \end{figure}

The module displayed above is constructed from the same hardware as the 3:2 compressor, but the third input $ z[k]$ of each adder is elimated, replaced by $ c[k]$ , the carry bit generated at index $ k-1$ . The resulting circuit, known as a ripple-carry adder, produces the sum of the two input vectors, $ x[n-1:0] + y[n-1:0]$ .

  (ripple-carry) Given $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ n \in \mathbb{N}$ , let $ c \in \mathbb{N}$ and $ s \in \mathbb{N}$ such that $ c[0] = 0$ and for $ k = 0,\ldots,n-1$ ,

$\displaystyle c[k+1] = x[k] \;\verb!&!\; y[k] \;\verb!\vert!\; x[k] \;\verb!&!\; c[k] \;\verb!\vert!\; y[k] \;\verb!&!\; c[k]$

and

$\displaystyle s[k] = x[k] \;\verb!^!\; y[k] \;\verb!^!\; c[k].$

Then

$\displaystyle x[n$-$\displaystyle 1:0] + y[n$-$\displaystyle 1:0] = \{c_n,s[n$-$\displaystyle 1:0].$

PROOF: We shall show that for $ 0 \leq k \leq n$ ,

$\displaystyle x[k$-$\displaystyle 1:0]+y[k$-$\displaystyle 1:0] = 2^kc_k + s[k$-$\displaystyle 1:0] = \{c_k,s[k$-$\displaystyle 1:0]\}.$

The claim is trivial for $ k = 0$ ; assume that it holds for some $ k$ , $ 0 \leq k < n$ . Then by Lemmas 2.3.13 and 6.1.3,
$\displaystyle x[k:0] + y[k:0]$ $\displaystyle =$ $\displaystyle 2^k(x[k] + y[k]) + x[k$-$\displaystyle 1:0]+y[k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 2^k(x[k] + y[k]) + 2^kc_k + s[k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 2^k(x[k] + y[k] + c_k) + s[k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 2^k\{c_{k\mbox{\rm +}1},s[k]\} + s[k\mbox{-}1:0]$  
  $\displaystyle =$ $\displaystyle 2^{k\mbox{\rm +}1}c_{k\mbox{\rm +}1} + 2^ks[k] + s[k\mbox{-}1:0]$  
  $\displaystyle =$ $\displaystyle 2^{k\mbox{\rm +}1}c_{k\mbox{\rm +}1} + s[k:0],$  

and the result follows by induction. 

Note that the execution time of the ripple-carry adder is a linear function of the width $ n$ of the input vectors, since the carry bit $ c[k-1]$ is required for the computation of $ c[k]$ and $ s[k]$ . 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 6.1.1   (gen) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ ,

$\displaystyle gen(x,y,i,j) = \left\{\begin{array}{ll} 0 & \mbox{if $i<j$}\\ x[... ...i\mbox{-}1,j) & \mbox{if $i \geq j$ and $x[i] \neq x[j]$.} \end{array}\right.$

Definition 6.1.2   (prop) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ ,

$\displaystyle prop(x,y,i,j) = \left\{\begin{array}{ll} 1 & \mbox{if $i < j$} ... ...i\mbox{-}1,j) & \mbox{if $i \geq j$ and $x[i] \neq x[j]$.} \end{array}\right.$

The value of $ gen(x,y,i,j)$ determines whether the sum $ x[i:j] + y[i:j]$ generates a carry out to bit $ i+1$ . In particular, according to the following lemma, the carry bit $ c[k]$ of Lemma 6.1.5 is given by

$\displaystyle c[k] = (x[k-1:0] + y[k-1:0])[k] = gen(x,y,k-1,0).$

  (gen-val) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ ,

$\displaystyle gen(x,y,i,j) = \left\{\begin{array}{ll} 1 & \mbox{if $x[i:j] + y[... ...{i+1-j}$}\\ 0 & \mbox{if $x[i:j] + y[i:j] < 2^{i+1-j}.$}\\ \end{array}\right.$

PROOF: By Lemma 2.3.13,

$\displaystyle x[i:j] = 2^{i-j}x[i] + x[i$-$\displaystyle 1:j]$

and

$\displaystyle y[i:j] = 2^{i-j}y[i] + y[i$-$\displaystyle 1:j].$

Thus, if $ x[i] = y[i] = 1$ , then $ gen(x,y,i,j) = 1$ and

$\displaystyle x[i:j] + y[i:j] \geq 2^{i-j} + 2^{i-j} = 2^{i+1-j},$

whereas if $ x[i] = y[i] = 0$ , then $ gen(x,y,i,j) = 0$ and by Lemma 2.2.1,

$\displaystyle x[i:j] + y[i:j] = x[i$-$\displaystyle 1:j] + y[i$-$\displaystyle 1:j] < 2^{i-j} + 2^{i-j} = 2^{i+1-j}.$

For the case $ x[i] \neq y[i]$ , we have

$\displaystyle 2^{i-j}x[i] + 2^{i-j}y[i] = 2^{i-j}.$

We proceed by induction on $ i-j$ , assuming that

$\displaystyle gen(x,y,i$-$\displaystyle 1,j) = 1 \Leftrightarrow x[i$-$\displaystyle 1:j] + y[i$-$\displaystyle 1:j] \geq 2^{i-j}.$

Suppose that $ gen(x,y,i$-$ 1,j) = 1$ . Then $ gen(x,y,i,j) = 1$ and

$\displaystyle x[i:j] + y[i:j] = 2^{i-j} + x[i$-$\displaystyle 1:j] + y[i$-$\displaystyle 1:j] \geq 2^{i-j} + 2^{i-j} = 2^{i+1-j}.$

On the other hand, if $ gen(x,y,i$-$ 1,j) = 0$ , then $ gen(x,y,i,j) = 0$ and

$\displaystyle x[i:j] + y[i:j] = 2^{i-j} + x[i$-$\displaystyle 1:j] + y[i$-$\displaystyle 1:j] < 2^{i-j} + 2^{i-j} = 2^{i+1-j}.$

Lemma 6.1.6 may be restated as follows.

  (gen-val-cor1) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ ,

$\displaystyle gen(x,y,i,j) = (x[i:j]+y[i:j])[i+1-j].$

PROOF: By Lemma 2.2.1,

$\displaystyle x[i:j]+y[i:j] < 2^{i+1-j} + 2^{i+1-j} = 2^{i+2-j}.$

Therefore, by Lemmas 2.3.9 and 2.3.18,

$\displaystyle (x[i:j]+y[i:j])[i+1-j] = 1 \Leftrightarrow x[i:j]+y[i:j] \geq 2^{i+1-j}.$

In the case $ j=0$ , we have the following equivalent formulation.

  (gen-val-cor2) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ i \in \mathbb{N}$ ,

$\displaystyle x[i:0] + y[i:0] = 2^{i+1}gen(x,y,i,0) + (x+y)[i:0].$

PROOF: By Lemma 2.2.1,

$\displaystyle x[i:0]+y[i:0] < 2^{i+1} + 2^{i+1} = 2^{i+2}.$

Thus, by Lemmas 2.2.11 and 2.3.13,
$\displaystyle x[i:0]+y[i:0]$ $\displaystyle =$ $\displaystyle (x[i:0]+y[i:0])[i+1:0]$  
  $\displaystyle =$ $\displaystyle 2^{i+1}(x[i:0]+y[i:0])[i+1] + (x[i:0]+y[i:0])[i:0].$  

But by Corollary 6.1.7,

$\displaystyle (x[i:0]+y[i:0])[i+1] = gen(x,y,i,0),$

and by Lemma 2.2.5,

$\displaystyle (x[i:0]+y[i:0])[i:0] = (x+y)[i:0].$

  (gen-special-case) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ , if $ i>j$ and

$\displaystyle (x[i:j] + y[i:j])[i$-$\displaystyle j] = 0,$

then

$\displaystyle gen(x,y,i,j) = x[i] \;\verb!\vert!\; y[i].$

PROOF: If $ x[i] \;\verb!\vert!\; y[i] = 0$ , then $ x[i] = y[i] = 0$ and by Lemmas 2.3.13 and 2.2.1,

$\displaystyle x[i:j] + y[i:j]$ $\displaystyle =$ $\displaystyle 2^{i\mbox{-}j}(x[i]+y[i]) + x[i\mbox{-}1:j] + y[i\mbox{-}1:j]$  
  $\displaystyle <$ $\displaystyle 2^{i\mbox{-}j} + 2^{i\mbox{-}j}$  
  $\displaystyle =$ $\displaystyle 2^{i\mbox{\rm +}1\mbox{-}j},$  

which implies $ gen(x,y,i,j) = 0$ .

Conversely, suppose that $ gen(x,y,i,j) = 0$ , so that

$\displaystyle x[i:j] + y[i:j] < 2^{i\mbox{\rm +}1\mbox{-}j}.$

Then $ x[i] = y[i] = 0$ , for otherwise we would have

$\displaystyle x[i:j] + y[i:j] = 2^{i\mbox{-}j}(x[i] + y[i]) + x[i\mbox{-}1:j] + y[i\mbox{-}1:j] \geq 2^{i\mbox{-}j},$

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

$\displaystyle (x[i:j] + y[i:j])[i$-$\displaystyle j] = 0.$

If $ gen(x,y,i,j) = 0$ , then $ prop(x,y,i,j)$ indicates whether a carry into bit $ j$ will be propagated out to bit $ i+1$ :

  (prop-val) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ , if $ i \geq j$ , then

$\displaystyle prop(x,y,i,j) = \left\{\begin{array}{ll} 1 & \mbox{if $x[i:j] + y... ...-1$}\\ 0 & \mbox{if $x[i:j] + y[i:j] \neq 2^{i+1-j}-1.$}\\ \end{array}\right.$

PROOF: By Lemmas 2.3.13 and 2.2.1,

$\displaystyle x[i:j] = 2^{i-j}x[i] + x[i$-$\displaystyle 1:j]$

and

$\displaystyle y[i:j] = 2^{i-j}y[i] + y[i$-$\displaystyle 1:j],$

where $ x[i$-$ 1:j] \leq 2^{i-j}-1$ and $ y[i$-$ 1:j] \leq 2^{i-j}-1$ . Through a simple case analysis, we conclude that

$\displaystyle x[i:j] + y[i:j] = 2^{i+1-j}-1 \Leftrightarrow x[i] \neq y[i]$    and $\displaystyle x[i$-$\displaystyle 1:j] + y[i$-$\displaystyle 1:j] = 2^{i-j}-1.$

Thus, if $ x[i] = y[i]$ , then $ x[i:j] + y[i:j] \neq 2^{i+1-j}-1$ and according to Definition 6.1.2, $ prop(x,y,i,j) = 0$ . Now suppose that $ x[i] \neq y[i]$ . Then by induction,
$\displaystyle x[i:j] + y[i:j] = 2^{i+1-j}-1$ $\displaystyle \Leftrightarrow$ $\displaystyle x[i$-$\displaystyle 1:j] + y[i$-$\displaystyle 1:j] = 2^{i-j}-1$  
  $\displaystyle \Leftrightarrow$ $\displaystyle prop(x,y,i$-$\displaystyle 1,j) = 1$  
  $\displaystyle \Leftrightarrow$ $\displaystyle prop(x,y,i,j) = 1.$  

  (prop-as-lxor) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ , if $ i \geq j$ , then

$\displaystyle prop(x,y,i,j) = 1 \Leftrightarrow x[i:j] \;\verb!^!\; y[i:j] = 2^{i+1-j}-1.$

PROOF: We shall show that

$\displaystyle x[i:j] \;\verb!^!\; y[i:j] = 2^{i+1-j}-1 \Leftrightarrow x[i:j] + y[i:j] = 2^{i+1-j}-1.$

The claim is trivial for $ i=j$ . Suppose $ i>j$ .

By Lemmas 3.2.9, and 2.2.20,

$\displaystyle (x[i:j] \;\verb!^!\; y[i:j])[i-j:0]$ $\displaystyle =$ $\displaystyle x[i:j][i-j:0] \;\verb!^!\; y[i:j][i-j:0]$  
  $\displaystyle =$ $\displaystyle x[i:j] \;\verb!^!\; y[i:j]$  

and
$\displaystyle (x[i:j] \;\verb!^!\; y[i:j])[i-j-1:0]$ $\displaystyle =$ $\displaystyle x[i:j][i-j-1:0] \;\verb!^!\; y[i:j][i-j-1:0]$  
  $\displaystyle =$ $\displaystyle x[i-1:j] \;\verb!^!\; y[i-1:j].$  

Similarly, by Lemmas 3.2.10, and 2.3.12,
$\displaystyle (x[i:j] \;\verb!^!\; y[i:j])[i-j]$ $\displaystyle =$ $\displaystyle x[i:j][i-j] \;\verb!^!\; y[i:j][i-j]$  
  $\displaystyle =$ $\displaystyle x[i] \;\verb!^!\; y[i].$  

Thus, by Lemma 2.3.13,
$\displaystyle x[i:j] \;\verb!^!\; y[i:j]$ $\displaystyle =$ $\displaystyle (x[i:j] \;\verb!^!\; y[i:j])[i-j:0]$  
  $\displaystyle =$ $\displaystyle 2^{i-j}(x[i] \;\verb!^!\; y[i]) + (x[i-1:j] \;\verb!^!\; y[i-1:j]).$  

But since

$\displaystyle x[i-1:j] \;\verb!^!\; y[i-1:j] = (x[i:j] \;\verb!^!\; y[i:j])[i-j-1:0] \leq 2^{i-j}-1,$

it follows that $ x[i:j] \;\verb!^!\; y[i:j] = 2^{i+1-j}-1$ if and only if

$\displaystyle x[i] \;\verb!^!\; y[i] = 1$    and $\displaystyle x[i-1:j] \;\verb!^!\; y[i-1:j] = 2^{i-j}-1,$

i.e.,

$\displaystyle x[i] \neq y[i]$    and $\displaystyle x[i-1:j] \;\verb!^!\; y[i-1:j] = 2^{i-j}-1.$

Therefore, by induction,

$\displaystyle x[i:j] \;\verb!^!\; y[i:j] = 2^{i+1-j}-1 \Leftrightarrow x[i] \neq y[i]$    and $\displaystyle x[i-1:j] + y[i-1:j] = 2^{i-j}-1.$

But as noted in the proof of Lemma 6.1.10,

$\displaystyle x[i:j] + y[i:j] = 2^{i+1-j}-1 \Leftrightarrow x[i] \neq y[i]$    and $\displaystyle x[i$-$\displaystyle 1:j] + y[i$-$\displaystyle 1:j] = 2^{i-j}-1.$

The computation of gen and prop may be facilitated by decomposing the interval $ [i,j]$ into subintervals.

  (gen-extend) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , $ j \in \mathbb{N}$ , and $ k \in \mathbb{N}$ , if $ i > k > j $ , then

$\displaystyle gen(x,y,i,j) = gen(x,y,i,k+1) \;\verb!\vert!\; prop(x,y,i.k+1) \;\verb!&!\; gen(x,y,k,j).$

PROOF: First suppose $ x[i] = y[i] = 1$ . By Definition 6.1.1, $ gen(x,y,i,j) = 1$ and $ gen(x,y,i,k+1) = 1$ , and each side of the equation reduces to $ 1$ .

Next, suppose $ x[i] = y[i] = 0$ . By Definition 6.1.1, $ gen(x,y,i,j) = 0$ and $ gen(x,y,i,k+1) = 0$ By Definition 6.1.2, $ prop(x,y,i,k+1) = 0$ , and each side of the equation reduces to 0 .

Thus, we may assume that $ x[i] \neq y[i]$ . By expanding the definitions, we reduce the equation to

$\displaystyle gen(x,y,i$-$\displaystyle 1,j) = gen(x,y,i$-$\displaystyle 1,k$+1$\displaystyle ) \;\verb!\vert!\; prop(x,y,i$-$\displaystyle 1.k$+$\displaystyle 1) \;\verb!&!\; gen(x,y,k,j).$

If $ i=k+1$ , then

$\displaystyle gen(x,y,i$-$\displaystyle 1,k$+1$\displaystyle ) = prop(x,y,i$-$\displaystyle 1.k$+1$\displaystyle ) = 0$

and the right-hand side further reduces to

$\displaystyle gen(x,y,k,j) = gen(x,y,i$-$\displaystyle 1,j).$

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

  (gen-extend-cor) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ , if $ i > k > j $ , then

$\displaystyle gen(x,y,i,j) = (x[i:k+1]+y[i:k+1]+gen(x,y,k,j))[i-k].$

PROOF: Since

$\displaystyle x[i:k+1]+y[i:k+1]+gen(x,y,k,j) \leq (2^{i\mbox{-}j}-1) + (2^{i\mbox{-}j}-1) + 1 < 2^{i\mbox{\rm +}1\mbox{-}j},$

it follows from Lemmas 2.3.9 and 2.3.18 that

$\displaystyle (x[i:k+1]+y[i:k+1]+gen(x,y,k,j))[i-k] = 1$

if and only if

$\displaystyle x[i:k+1]+y[i:k+1]+gen(x,y,k,j) \geq 2^{i\mbox{-}k}.$

But this inequality holds if and only if either

$\displaystyle x[i:k+1]+y[i:k+1] \geq 2^{i\mbox{-}k}$

or

$\displaystyle x[i:k+1]+y[i:k+1] = 2^{i\mbox{-}k} \mbox{ and } gen(x,y,k,j) = 1.$

Applying Lemmas 6.1.6 and 6.1.10, we may write this disjunction as

$\displaystyle gen(x,y,i,k+1) \;\verb!\vert!\; prop(x,y,i,k+1) \;\verb!&!\; gen(x,y,k,j) = 1,$

which, according to Lemma 6.1.12, reduces to

$\displaystyle gen(x,y,i,j) = 1.$

  (prop-extend) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , $ j \in \mathbb{N}$ , and $ k \in \mathbb{N}$ , if $ i > k > j $ , then

$\displaystyle prop(x,y,i,j) = prop(x,y,i,k+1) \;\verb!&!\; prop(x,y,k,j).$

PROOF: If $ x[i] = y[i]$ , then $ prop(x,y,i,j) = prop(x,y,i,k+1) = 0$ . Thus, we may assume $ x[i] \neq y[i]$ . In this case, the equation reduces to

$\displaystyle prop(x,y,i-i,j) = prop(x,y,i-1,k+1) \;\verb!&!\; prop(x,y,k,j).$

If $ i=k+1$ , then $ prop(x,y,i-i,j) = prop(x,y,i$-$ 1,k+1) = 0$ . In the remaining case, the proof is completed by induction. 


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

$\displaystyle p[k] = x[k] \;\verb!^!\; y[k] = prop(x,y,k,k)$

and

$\displaystyle g[k] = x[k] \;\verb!&!\; y[k] = gen(x,y,k,k).$

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


$\displaystyle prop(x,y,i,j)$ $\displaystyle =$ $\displaystyle p[i] \;\verb!&!\; prop(x,y,i-1,j)$  
  $\displaystyle =$ $\displaystyle p[i] \;\verb!&!\; p[i-1] \;\verb!&!\; prop(x,y,i-2,j)$  
  $\displaystyle =$ $\displaystyle \cdots$  
  $\displaystyle =$ $\displaystyle p[i] \;\verb!&!\; p[i-1] \cdots \;\verb!&!\; p[j],$  

and by Lemma 6.1.12,
$\displaystyle gen(x,y,j+1,j)$ $\displaystyle =$ $\displaystyle g[j+1] \;\verb!\vert!\; p[j+1] \;\verb!&!\; g[j],$  
       
$\displaystyle gen(x,y,j+2,j)$ $\displaystyle =$ $\displaystyle g[j+2] \;\verb!\vert!\; p[j+2] \;\verb!&!\; gen(x,y,j+1,j)$  
  $\displaystyle =$ $\displaystyle g[j+2] \;\verb!\vert!\; p[j+2] \;\verb!&!\; g[j+1] ;\verb!\vert!\; p[j+2] \;\verb!&!\; p[j+1] \;\verb!&!\; g[j],$  
$\displaystyle \cdots$      
$\displaystyle gen(x,y,i,j)$ $\displaystyle =$ $\displaystyle g[i] \;\verb!\vert!\; p[i] \;\verb!&!\; gen(x,y,i-1,j)$  
  $\displaystyle =$ $\displaystyle g[i] \;\verb!\vert!\; p[i] \;\verb!&!\; g[i-1] \;\verb!\vert!\; p[i] \;\verb!&!\; p[i-1] \;\verb!&!\; gen(x,y,i-2,j)$  
  $\displaystyle =$ $\displaystyle \cdots$  
  $\displaystyle =$ $\displaystyle g[i] \;\verb!\vert!\; p[i] \;\verb!&!\; g[i-1] \;\verb!\vert!\; \cdots \;\verb!\vert!\;$  
           $\displaystyle p[i] \;\verb!&!\; p[i-1] \;\verb!&!\; \cdots \;\verb!&!\; p[j+1] \;\verb!&!\; g[j].$  

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

(1) 1 gate delay to compute the generate and propagate bits,

$\displaystyle g[k] = x[k] \;\verb!&!\; y[k]$

and

$\displaystyle p[k] = x[k] \;\verb!^!\; y[k],$

(2) 2 gate delays to compute the carry bits

$\displaystyle c[k] = gen(x,y,k-1,0)$

using the above equation, and

(3) 1 gate delay to compute the sum $ s = x+y$ using the formula

$\displaystyle s[k] = x[k] \;\verb!^!\; y[k] \;\verb!^!\; c[k].$

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

  (bits-sum) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ ,

$\displaystyle (x+y)[i:j] = (x[i:j] + y[i:j] + gen(x,y,j$-$\displaystyle 1,0))[i-j:0].$

PROOF: By Lemma 2.3.13 and Corollary 6.1.8,

$\displaystyle x[i:0]+y[i:0]$ $\displaystyle =$ $\displaystyle 2^j(x[i:j] + y[i:j]) + x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 2^j(x[i:j] + y[i:j] + gen(x,y,j$-$\displaystyle 1,0)) + (x+y)[j$-$\displaystyle 1:0].$  

By Lemma 2.2.1, $ (x+y)[j$-$ 1:0] < 2^j$ , and hence

$\displaystyle \lfloor (x[i:0] + y[i:0])/2^j \rfloor x[i:j] + y[i:j] + gen(x,y,j$-$\displaystyle 1,0).$

Now by Lemmas 2.2.20, 2.2.5, and 2.2.13,
$\displaystyle (x+y)[i:j]$ $\displaystyle =$ $\displaystyle (x+y)[i:0][i:j]$  
  $\displaystyle =$ $\displaystyle (x[i:0]+y[i:0])[i:0][i:j]$  
  $\displaystyle =$ $\displaystyle (x[i:0]+y[i:0])[i:j]$  
  $\displaystyle =$ $\displaystyle \lfloor (x[i:0]+y[i:0])/2^j \rfloor[i-j:0]$  
  $\displaystyle =$ $\displaystyle (x[i:j] + y[i:j] + gen(x,y,j$-$\displaystyle 1,0))[i-j:0].$  

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

  (bits-sum-swallow) Let $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , $ j \in \mathbb{N}$ , and $ k \in \mathbb{N}$ . If $ i \geq j > k$ , $ x[k] = 0$ , and $ y \leq 2^k$ , then

$\displaystyle (x+y)[i:j] = x[i:j].$

PROOF: Since $ y < 2^{k\mbox{\rm +}1}$ , Lemmas 2.2.11 and 2.2.19 imply

$\displaystyle y = y[i:0] = 2^ky[i:k$+$\displaystyle 1]+y[k:0] = y[k:0],$

and hence $ y[i:k$+$ 1] = 0$ . Since $ x[k] = 0$ ,

$\displaystyle x[k:0] = x[k$-$\displaystyle 1:0] < 2^k$

by Lemmas 2.3.13 and 2.2.1. Hence,

$\displaystyle x[k:0] + y[k:0] < 2^k + 2^k = 2^{k\mbox{\rm +}1}$

and

$\displaystyle gen(x,y,k,0) = (x[k:0] + y[k:0])[k$+$\displaystyle 1] = 0.$

By Lemmas 6.1.15 and 2.2.20,
$\displaystyle (x+y)[i:k$+$\displaystyle 1]$ $\displaystyle =$ $\displaystyle (x[i:k$+$\displaystyle 1] + y[i:k$+$\displaystyle 1])[i$-$\displaystyle k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (x[i:k$+$\displaystyle 1])[i$-$\displaystyle k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle x[i:k$+$\displaystyle 1].$  

Finally, by Lemma 2.2.20,
$\displaystyle (x+y)[i:j]$ $\displaystyle =$ $\displaystyle (x+y)[i:k$+$\displaystyle 1][i$-$\displaystyle k$-$\displaystyle 1:j$-$\displaystyle k$-$\displaystyle 1]$  
  $\displaystyle =$ $\displaystyle x[i:k$+$\displaystyle 1][i$-$\displaystyle k$-$\displaystyle 1:j$-$\displaystyle k$-$\displaystyle 1]$  
  $\displaystyle =$ $\displaystyle x[i:j].$  

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

  (bits-sum-cor) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ , if

$\displaystyle gen(x,y,i,j) = gen(x,y,j$-$\displaystyle 1,0) = 0,$

then

$\displaystyle (x+y)[i:j] = x[i:j] + y[i:j].$

PROOF: By Lemma 6.1.15,

$\displaystyle (x+y)[i:j] = (x[i:j] + y[i:j])[i$-$\displaystyle j:0].$

But by Lemma 6.1.6, $ x[i:j] + y[i:j] < 2^{i\mbox{\rm +}1\mbox{-}j},$ and hence by Lemma 2.2.11,

$\displaystyle (x[i:j] + y[i:j])[i$-$\displaystyle j:0] = x[i:j] + y[i:j].$

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

  (bits-sum-3) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ z \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ ,
$\displaystyle (x+y+z)[i:j]$ $\displaystyle =$ $\displaystyle (x[i:j] + y[i:j] + z[i:j]$  
    $\displaystyle + gen(x,y,j$-$\displaystyle 1,0) + gen(x+y,z,j$-$\displaystyle 1,0))[i-j:0].$  

PROOF: Applying Lemma 6.1.15 twice and appealing to Corollary 2.2.5, we have

$\displaystyle (x+y+z)[i:j]$ $\displaystyle =$ $\displaystyle ((x+y) + z)[i:j]$  
  $\displaystyle =$ $\displaystyle ((x+y)[i:j] + z[i:j] + gen(x+y,z,j-1,0))[i$-$\displaystyle j:0]$  
  $\displaystyle =$ $\displaystyle ((x[i:j]+y[i:j] + gen(x,y,j-1,0))[i$-$\displaystyle j]$  
    $\displaystyle + z[i:j] + gen(x+y,z,j$-$\displaystyle 1,0))[i$-$\displaystyle j:0]$  
  $\displaystyle =$ $\displaystyle (x[i:j]+y[i:j] + gen(x,y,j-1,0) + z[i:j]$  
    $\displaystyle + gen(x+y,z,j$-$\displaystyle 1,0))[i$-$\displaystyle j:0].$  

The case $ z=1$ is of particular interest.

  (bits-sum-plus-1) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ z \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ ,

$\displaystyle (x+y+1)[i:j] = (x[i:j] + y[i:j] + prop(x,y,j$-$\displaystyle 1,0) \;\verb!\vert!\; gen(x,y,j$-$\displaystyle 1,0))[i-j:0].$

PROOF: By Lemma 6.1.18, it suffices to show that

$\displaystyle prop(x,y,j$-$\displaystyle 1,0) \;\verb!\vert!\; gen(x,y,j$-$\displaystyle 1,0) = gen(x,y,j$-$\displaystyle 1,0) + gen(x+y,1,j$-$\displaystyle 1,0).$

Suppose first that $ gen(x,y,j$-$ 1,0) = 1$ . By Lemma 2.2.1,

$\displaystyle x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0] \leq (2^j-1)+(2^j-1) < 2^{j\mbox{\rm +}1}-1.$

Thus, by Lemma 2.2.11, Lemma 2.3.13, Corollary 6.1.7, and Corollary 2.2.5,
$\displaystyle 2^{j\mbox{\rm +}1}-1$ $\displaystyle >$ $\displaystyle x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0])[j:0]$  
  $\displaystyle =$ $\displaystyle 2^j(x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0])[j] + (x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0])[j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 2^jgen(x,y,j$-$\displaystyle 1,0) + (x + y)[j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 2^j + (x + y)[j$-$\displaystyle 1:0],$  

and hence $ (x+y)[j$-$ 1:0] < 2^j-1$ . It follows that $ gen(x+y,1,j$-$ 1,0) = 0$ , and both sides of our equation reduce to 1.

Now suppose that $ gen(x,y,j$-$ 1,0) = 0$ . In this case, we must show that

$\displaystyle prop(x,y,j$-$\displaystyle 1,0) = gen(x+y,1,j$-$\displaystyle 1,0).$

By Lemma 6.1.6,

$\displaystyle x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0] < 2^j,$

and hence, by Corollary 2.2.5 and Lemma 2.2.11,

$\displaystyle (x+y)[j$-$\displaystyle 1:0] = (x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0])[j$-$\displaystyle 1:0] = x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0].$

Now
$\displaystyle prop(x,y,j$-$\displaystyle 1,0) = 1$ $\displaystyle \Leftrightarrow$ $\displaystyle x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0] = 2^j-1$  
  $\displaystyle \Leftrightarrow$ $\displaystyle x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0] \geq 2^j-1$  
  $\displaystyle \Leftrightarrow$ $\displaystyle x[j$-$\displaystyle 1:0] + y[j$-$\displaystyle 1:0]+1 \geq 2^j$  
  $\displaystyle \Leftrightarrow$ $\displaystyle (x+y)[j$-$\displaystyle 1:0]+1 \geq 2^j$  
  $\displaystyle \Leftrightarrow$ $\displaystyle gen(x+y,1,j$-$\displaystyle 1,0) = 1.$  

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.

  (land-gen-0) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ , if

$\displaystyle x[i:j] \;\verb!&!\; y[i:j] = 0,$

then

$\displaystyle gen(x,y,i,j) = 0.$

PROOF: The proof is by induction on $ i$ . The case $ i < j$ is trivial. For $ \geq j$ , by Lemma 6.1.12,

$\displaystyle gen(x,y,i,j) = gen(x,y,i,i) \;\verb!\vert!\; prop(x,y,i,i) \;\verb!&!\; gen(x,y,i-1,j).$

We shall show that $ gen(x,y,i,i) = gen(x,y,i-1,j) = 0$ .

By Lemmas 2.3.12, 3.2.10, and 2.3.5,

$\displaystyle x[i] \;\verb!&!\; y[i]$ $\displaystyle =$ $\displaystyle x[i:j][i$-$\displaystyle j] \;\verb!&!\; y[i:j][i$-$\displaystyle j]$  
  $\displaystyle =$ $\displaystyle (x[i:j] \;\verb!&!\; y[i:j])[i$-$\displaystyle j]$  
  $\displaystyle =$ $\displaystyle 0[i$-$\displaystyle j]$  
  $\displaystyle =$ $\displaystyle 0.$  

It follows that either $ x[i] \neq y[i]$ or $ x[i] = 0$ . In either case, by Definition 6.1.1,

$\displaystyle gen(x,y,i,i) = gen(x,y,i-1,i) = 0.$

Similarly, by Lemmas 2.2.20, 3.2.10, and 2.2.10,
$\displaystyle x[i$-$\displaystyle 1:j] \;\verb!&!\; y[i$-$\displaystyle 1:j]$ $\displaystyle =$ $\displaystyle x[i:j][i$-$\displaystyle j$-$\displaystyle 1:0] \;\verb!&!\; y[i:j][i$-$\displaystyle j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (x[i:j] \;\verb!&!\; y[i:j])[i$-$\displaystyle j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 0[i$-$\displaystyle j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 0.$  

By induction, therefore, $ gen(x,y,i-1,j) = 0$ . 

  (land-gen-0-cor) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ , if

$\displaystyle x[i:0] \;\verb!&!\; y[i:0] = 0,$

then

$\displaystyle (x+y)[i:j] = x[i:j] + y[i:j].$

PROOF: We may assume $ i \geq j$ . By Lemmas 2.2.20, 3.2.10, and 2.2.10,

$\displaystyle x[j$-$\displaystyle 1:0] \;\verb!&!\; y[j$-$\displaystyle 1:0]$ $\displaystyle =$ $\displaystyle x[i:0][j$-$\displaystyle 1:0] \;\verb!&!\; y[i:0][j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (x[i:0] \;\verb!&!\; y[i:0])[j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 0[j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle 0.$  

Thus, by Lemma 6.1.15,

$\displaystyle (x+y)[i:j] = (x[i:j] + y[i:j])[i$-$\displaystyle j:0].$

Similarly,
$\displaystyle x[i:j] \;\verb!&!\; y[i:j]$ $\displaystyle =$ $\displaystyle x[i:0][i:j] \;\verb!&!\; y[i:0][i:j]$  
  $\displaystyle =$ $\displaystyle (x[i:0] \;\verb!&!\; y[i:0])[i:j]$  
  $\displaystyle =$ $\displaystyle 0[i:j]$  
  $\displaystyle =$ $\displaystyle 0,$  

and $ x[i:j] + y[i:j] < 2^{i\mbox{\rm +}1\mbox{-}j}$ by Lemmas 6.1.20 and 6.1.6. Thus, by Lemma 2.2.11,

$\displaystyle (x[i:j] + y[i:j])[i$-$\displaystyle j:0] = x[i:j] + y[i:j].$

  (gen-plus) Let $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ z \in \mathbb{N}$ , and $ k \in \mathbb{N}$ . If $ z < 2^{k+1}$ , $ z[k:0] \;\verb!&!\; y[k:0] = 0$ , and $ gen(x,y,k,0) = 1$ , then $ gen(x+y, z, k, 0) = 0$ .

PROOF: By Corollary 6.1.8,

$\displaystyle x[k:0] + y[k:0] = 2^{k+1} + (x + y)[k:0].$

Thus, by Corollary 6.1.21 and Lemma 2.2.1,
$\displaystyle (x + y)[k:0] + z[k:0]$ $\displaystyle =$ $\displaystyle x[k:0] + y[k:0] - 2^{k+1} + z[k:0]$  
  $\displaystyle =$ $\displaystyle x[k:0] + (y + z)[k:0] - 2^{k+1}$  
  $\displaystyle <$ $\displaystyle 2^{k+1} + 2^{k+1} - 2^{k+1}$  
  $\displaystyle =$ $\displaystyle 2^{k+1}.$  

The lemma follows from Lemma 6.1.6. 

  (gen-extend-3) Let $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ with $ i>j$ . Let $ z$ be a $ (j+1)$ -bit vector such that

$\displaystyle y[j:0] \;\verb!&!\; z[j:0] = 0.$

Then

$\displaystyle gen(x+y,z,i,0) = prop(x,y,i,j+1) \;\verb!&!\; gen(x+y,z,j,0).$

PROOF: Since $ z[i:j+1] = 0$ , it is clear from Lemma 6.1.6 that

$\displaystyle gen(x+y, z, i, j+1) = 0.$

Thus, by Lemma 6.1.12,

$\displaystyle gen(x+y,z,i,0) = prop(x+y,z,i,j+1) \;\verb!&!\; gen(x+y,z,j,0).$

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

$\displaystyle prop(x+y, z, i, j+1) = prop(x, y, i, j+1).$

By Lemma 6.1.22, $ gen(x, y, j, 0) = 0$ , and by Lemma 6.1.15,
$\displaystyle (x+y)[i:j+1]$ $\displaystyle =$ $\displaystyle (x[i:j+1] + y[i:j+1] + gen(x, y, j, 0))[i$-$\displaystyle j$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (x[i:j+1] + y[i:j+1])[i$-$\displaystyle j$-$\displaystyle 1:0].$  

Thus, by Lemma 6.1.10,
$\displaystyle prop(x+y, z, i, j+1) = 1$ $\displaystyle \Leftrightarrow$ $\displaystyle (x+y)[i:j+1] + z[i:j+1] = 2^{i\mbox{-}j}-1$  
  $\displaystyle \Leftrightarrow$ $\displaystyle (x+y)[i:j+1] = 2^{i\mbox{-}j}-1$  
  $\displaystyle \Leftrightarrow$ $\displaystyle (x[i:j+1] + y[i:j+1])[i$-$\displaystyle j$-$\displaystyle 1:0] = 2^{i\mbox{-}j}-1,$  

whereas

$\displaystyle prop(x, y, i, j+1) = 1 \Leftrightarrow (x[i:j+1] + y[i:j+1]) = 2^{i\mbox{-}j}-1.$

It remains to show that

$\displaystyle (x[i:j+1] + y[i:j+1])[i$-$\displaystyle j$-$\displaystyle 1:0] = 2^{i\mbox{-}j}-1 \Leftrightarrow x[i:j+1] + y[i:j+1] = 2^{i\mbox{-}j}-1.$

Suppose first that

$\displaystyle (x[i:j+1] + y[i:j+1])[i$-$\displaystyle j$-$\displaystyle 1:0] = 2^{i\mbox{-}j}-1.$

By Lemma 2.2.1,

$\displaystyle x[i:j+1] + y[i:j+1] \leq (2^{i\mbox{-}j}-1) + (2^{i\mbox{-}j}-1) < 2^{i\mbox{\rm +}1\mbox{-}j}-1.$

Therefore, by Lemmas 2.2.11 and 2.3.13,
$\displaystyle {x[i:j+1] + y[i:j+1]}$
  $\displaystyle =$ $\displaystyle (x[i:j+1] + y[i:j+1])[i$-$\displaystyle j:0]$  
  $\displaystyle =$ $\displaystyle 2^{i\mbox{-}j}(x[i:j+1] + y[i:j+1])[i\mbox{-}j] + (x[i:j+1] + y[i:j+1])[i\mbox{-}j\mbox{-}1:0]$  
  $\displaystyle =$ $\displaystyle 2^{i\mbox{-}j}(x[i:j+1] + y[i:j+1])[i\mbox{-}j] + 2^{i\mbox{-}j}-1.$  

But by Lemma 2.2.1,

$\displaystyle x[i:j+1] + y[i:j+1] \leq (2^{i\mbox{-}j}-1) + (2^{i\mbox{-}j}-1) < 2^{i\mbox{-}j} + 2^{i\mbox{-}j}-1,$

which implies $ (x[i:j+1] + y[i:j+1])[i$-$ j] = 0$ , and hence

$\displaystyle x[i:j+1] + y[i:j+1] = 2^{i\mbox{-}j}-1.$

On the other hand, if

$\displaystyle x[i:j+1] + y[i:j+1] = 2^{i\mbox{-}j}-1 < 2^{i\mbox{-}j},$

then

$\displaystyle x[i:j+1] + y[i:j+1] = (x[i:j+1] + y[i:j+1])[i$-$\displaystyle j$-$\displaystyle 1:0]$

by Lemma 2.2.11. 

next up previous contents
Next: Leading One Prediction Up: Addition Previous: Addition   Contents
David Russinoff 2007-01-02