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

Trailing One Prediction

As we saw in Chapter 6, the process of rounding a bit vector often involves determining its degree of exactness. For this purpose, therefore, it is also useful to predict the trailing one of a sum, i.e., the least index at which a one occurs. The following lemmas provide methods for computing, in constant time, an integer that has precisely the same trailing one as the sum or difference of two given operands.

Note that the difference $ x-y$ of $ n$ -bit vectors $ x$ and $ y$ is commonly computed as a sum, using the identity $ \verb! !y[n$-$ 1:0] = 2^n-y[n$-$ 1:0]-1$ , which leads to the formula

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

Thus, we are also interested in computing the trailing one of an incremented sum. This problem admits a particularly simple solution.

  (top-thm-1) Let $ a$ and $ b$ be n-bit vectors, where $ n \in \mathbb{N}$ . For all $ k \in
\mathbb{N}$ , if $ k<n$ , then

$\displaystyle (a+b+1)[k:0] = 0 \Leftrightarrow \verb! !(a \;\verb!^!\; b)[k:0] = 0.$

PROOF: First we consider the case $ k=0$ . By Corollary 2.2.9,

$\displaystyle (a+b+1)[0] = (a[0]+b[0]+1)[0],$

and exhaustive testing yields

$\displaystyle (a[0]+b[0]+1)[0] = \verb! !(a[0] \;\verb!^!\; b[0]).$

Thus, by Lemmas 3.2.5 and 3.1.13,

$\displaystyle \verb! !(a[0] \;\verb!^!\; b[0]) = \verb! !(a \;\verb!^!\; b)[0] = (a+b+1)[0].$

We proceed by induction, assuming $ k>0$ . Using Lemma 2.2.21 in the form

$\displaystyle x[k:0] = 2x[k:1] + x[0],$

we may assume that

$\displaystyle (a+b+1)[0] = \verb! !(a[0] \;\verb!^!\; b[0]) = 0$

and need only show that

$\displaystyle (a+b+1)[k:1] = 0 \Leftrightarrow \verb! !(a[n$-$\displaystyle 1:0] \;\verb!^!\; b[n$-$\displaystyle 1:0])[k:1] = 0.$

Let $ a' = a[n$-$ 1:1]$ and $ b' = b[n$-$ 1:1]$ . By inductive hypothesis,

$\displaystyle (a'+b'+1)[k$-$\displaystyle 1:0] = 0 \Leftrightarrow \verb! !(a'[n$-$\displaystyle 2:0] \;\verb!^!\; b'[n$-$\displaystyle 2:0])[k$-$\displaystyle 1:0] = 0.$

By Lemmas 2.2.22, 3.2.4, and 3.1.12,
$\displaystyle \verb! !(a[n$-$\displaystyle 1:0] \;\verb!^!\; b[n$-$\displaystyle 1:0])[k:1]$ $\displaystyle =$ $\displaystyle \verb! !(a[k:1] \;\verb!^!\; b[k:1])$  
  $\displaystyle =$ $\displaystyle \verb! !(a'[k$-$\displaystyle 1:0] \;\verb!^!\; b'[k$-$\displaystyle 1:0])$  
  $\displaystyle =$ $\displaystyle \verb! !(a'[n$-$\displaystyle 2:0] \;\verb!^!\; b'[n$-$\displaystyle 2:0])[k$-$\displaystyle 1:0].$  

Therefore, it suffices to show that

$\displaystyle (a+b+1)[k:1] = (a'+b'+1)[k$-$\displaystyle 1:0].$

Note that since $ \verb! !(a[0] \;\verb!^!\; b[0]) = 0$ , $ a[0]+b[0] = 1$ , and it follows that

$\displaystyle prop(a,b,0,0) = 1.$

Thus, by Lemmas 7.1.19 and 2.2.22 and Corollary 2.2.9,


$\displaystyle (a+b+1)[k:1]$ $\displaystyle =$ $\displaystyle (a[k:1] + b[k:1] + 1)[k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (a'[k$-$\displaystyle 1:0] + b'[k$-$\displaystyle 1:0] + 1)[k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (a'+b'+1)[k$-$\displaystyle 1:0].$  

Our next lemma is applicable to both addition and subtraction, but involves a somewhat more complicated computation.

  (top-thm-2) Let $ a$ and $ b$ be n-bit vectors, where $ n \in \mathbb{N}$ , and let $ c$ be a 1-bit vector. Let

$\displaystyle \tau = \{1\verb!'b!0, a[n$-$\displaystyle 1:0] \;\verb!^!\; b[n$-$\displaystyle 1:0]\} \;\verb!^!\;
\{a[n$-$\displaystyle 1:0] \;\verb!\vert!\; b[n$-$\displaystyle 1:0], c\}.$

Then for all $ k \in
\mathbb{N}$ , if $ k<n$ , then

$\displaystyle (a+b+c)[k:0] = 0 \Leftrightarrow \tau[k:0] = 0.$

PROOF: Exhaustive testing yields

$\displaystyle (a[0]+b[0]+c)[0] = a[0] \;\verb!^!\; b[0] \;\verb!^!\; c,$

and hence, by Corollary 2.2.9,

$\displaystyle (a+b+1)[0] = (a[0]+b[0]+1)[0] = a[0] \;\verb!^!\; b[0] \;\verb!^!\; c.$

By Lemmas 3.1.13, 2.4.7, and 2.3.16,
$\displaystyle \tau[0]$ $\displaystyle =$ $\displaystyle \{1\verb!'b!0, a[n$-$\displaystyle 1:0] \;\verb!^!\; b[n$-$\displaystyle 1:0]\}[0] \;\verb!^!\;
\{a[n$-$\displaystyle 1:0] \;\verb!\vert!\; b[n$-$\displaystyle 1:0], c\}[0]$  
  $\displaystyle =$ $\displaystyle \{1\verb!'b!0, a[n$-$\displaystyle 1:0] \;\verb!^!\; b[n$-$\displaystyle 1:0]\}[n$-$\displaystyle 1:0][0] \;\verb!^!\;
\{a[n$-$\displaystyle 1:0] \;\verb!\vert!\; b[n$-$\displaystyle 1:0], c\}[0]$  
  $\displaystyle =$ $\displaystyle (a \;\verb!^!\; b)[0] \;\verb!^!\; c$  
  $\displaystyle =$ $\displaystyle a[0] \;\verb!^!\; b[0] \;\verb!^!\; c$  
  $\displaystyle =$ $\displaystyle (a+b+1)[0].$  

This establishes the case $ k=0$ . For $ k>0$ , we proceed by induction. Using Lemma 2.2.21 in the form

$\displaystyle x[k:0] = 2x[k:1] + x[0],$

we may assume that

$\displaystyle (a+b+c)[0] = \tau[0] = 0$

and need only show that

$\displaystyle (a+b+c)[k:1] = 0 \Leftrightarrow \tau[k:1] = 0.$

Let $ a' = a[n$-$ 1:1]$ $ b' = b[n$-$ 1:1]$ , $ c = a[0] \;\verb!\vert!\; b[0]$ , and
$\displaystyle \tau'$ $\displaystyle =$ $\displaystyle \tau[n:1]$  
  $\displaystyle =$ $\displaystyle \{1\verb!'b!0, a[n$-$\displaystyle 1:0] \;\verb!^!\; b[n$-$\displaystyle 1:0]\}[n:1] \;\verb!^!\;
\{a[n$-$\displaystyle 1:0] \;\verb!\vert!\; b[n$-$\displaystyle 1:0], c\}[n:1].$  

By Lemmas 3.1.12 and 2.2.22,
$\displaystyle \{1\verb!'b!0, a[n$-$\displaystyle 1:0] \;\verb!^!\; b[n$-$\displaystyle 1:0]\}[n:1]$ $\displaystyle =$ $\displaystyle (a \;\verb!^!\; b)[n:1]$  
  $\displaystyle =$ $\displaystyle a[n$-$\displaystyle 1:0][n:1] \;\verb!^!\; b[n$-$\displaystyle 1:0][n:1]$  
  $\displaystyle =$ $\displaystyle a[n$-$\displaystyle 1:1] \;\verb!^!\; b[n$-$\displaystyle 1:1]$  
  $\displaystyle =$ $\displaystyle \{1\verb!'b!0, a[n$-$\displaystyle 1:1] \;\verb!^!\; b[n$-$\displaystyle 1:1]\}$  

and by Lemmas 2.4.7, 2.4.9, 3.1.6, and 2.2.22,
$\displaystyle \{a[n$-$\displaystyle 1:0] \;\verb!\vert!\; b[n$-$\displaystyle 1:0], c\}[n:1]$ $\displaystyle =$ $\displaystyle a \;\verb!\vert!\; b$  
  $\displaystyle =$ $\displaystyle \{a[n$-$\displaystyle 1:1],a[0]\} \;\verb!\vert!\; \{b[n$-$\displaystyle 1:1],b[0]\}$  
  $\displaystyle =$ $\displaystyle \{a[n$-$\displaystyle 1:1] \;\verb!\vert!\; b[n$-$\displaystyle 1:1],a[0] \;\verb!\vert!\; b[0]\}$  
  $\displaystyle =$ $\displaystyle \{a'[n$-$\displaystyle 2:0] \;\verb!\vert!\; b'[n$-$\displaystyle 2:0], c'\}.$  

Thus,

$\displaystyle \tau' = \{1\verb!'b!0, a[n$-$\displaystyle 1:1] \;\verb!^!\; b[n$-$\displaystyle 1:1]\} \;\verb!^!\;
\{a'[n$-$\displaystyle 2:0] \;\verb!\vert!\; b'[n$-$\displaystyle 2:0], c'\}.$

By inductive hypothesis,

$\displaystyle (a'+b'+c')[k$-$\displaystyle 1:0] = 0 \Leftrightarrow \tau'[k$-$\displaystyle 1:0] = 0.$

But

$\displaystyle \tau'[k$-$\displaystyle 1:0] = \tau[n:1][k$-$\displaystyle 1:0] = \tau[k:1].$

Thus, it will suffice to show that

$\displaystyle (a+b+c)[k:1] = (a'+b'+c')[k$-$\displaystyle 1:0].$

Suppose first that $ c=0$ . Then $ a[0] = b[0]$ and it follows that

$\displaystyle c' = a[0] \;\verb!&!\; b[0] = gen(a,b,0,0).$

By Lemma 7.1.15 and Corollary 2.2.9,
$\displaystyle (a+b+c)[k:1]$ $\displaystyle =$ $\displaystyle (a+b)[k:1]$  
  $\displaystyle =$ $\displaystyle (a[k:1] + b[k:1] + c')[k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (a'[k$-$\displaystyle 1:0] + b'[k$-$\displaystyle 1:0] + c')[k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (a'+b'+c')[k$-$\displaystyle 1:0].$  

Finally, suppose that $ c=1$ . Then $ a[0] \neq b[0]$ and hence $ a[0]+b[0] = 1$ , which implies that $ gen(a,b,0,0) = 0$ and

$\displaystyle c' = a[0] \;\verb!\vert!\; b[0] = prop(a,b,0,0) = prop(a,b,0,0) \;\verb!\vert!\; gen(a,b,0,0).$

By Lemmas 7.1.19 and 2.2.22 and Corollary 2.2.9,
$\displaystyle (a+b+c)[k:1]$ $\displaystyle =$ $\displaystyle (a+b+1)[k:1]$  
  $\displaystyle =$ $\displaystyle (a[k:1] + b[k:1] + c')[k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (a'[k$-$\displaystyle 1:0] + b'[k$-$\displaystyle 1:0] + c')[k$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle (a'+b'+c')[k$-$\displaystyle 1:0].$  


next up previous contents
Next: Multiplication Up: Addition Previous: Leading One Prediction   Contents
david.m.russinoff 2015-02-08