next up previous contents
Next: Algebraic Properties Up: Logical Operations Previous: Complementation   Contents

Binary Operations

There are three primitive RTL binary logical operations, which we define recursively.

Definition 3.2.1   (binary-land) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ n \in \mathbb{N}$ ,

$\displaystyle land(x,y,n) = \left\{\begin{array}{ll} 0 & \mbox{if $n=0$}\\ 2 \... ...loor, \lfloor y/2 \rfloor, n\mbox{-}1) & \mbox{otherwise}. \end{array} \right.$

Definition 3.2.2   (binary-lior) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ n \in \mathbb{N}$ ,

$\displaystyle lior(x,y,n) = \left\{\begin{array}{ll} 0 & \mbox{if $n=0$}\\ 2 \... ...r, \lfloor y/2 \rfloor, n\mbox{-}1) +1 & \mbox{otherwise}. \end{array} \right.$

Definition 3.2.3   (binary-lxor) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ n \in \mathbb{N}$ ,

$\displaystyle lxor(x,y,n) = \left\{\begin{array}{ll} 0 & \mbox{if $n=0$}\\ 2 \... ...or, \lfloor y/2 \rfloor, n\mbox{-}1)+1 & \mbox{otherwise}. \end{array} \right.$

We first note the trivial case $ n=0$ .

Lemma 3.2.1   (land-x-y-0, lior-x-y-0, lxor-x-y-0)
For all $ x \in \mathbb{N}$ and $ y \in \mathbb{N}$ ,

(b) $ land(x,y,0) = 0$
(c) $ lior(x,y,0) = 0$
(d) $ lxor(x,y,0) = 0$ .

The operands may be truncated without affecting the result.

  (land-bits-1, land-bits-2, lior-bits-1,lior-bits-2,
lxor-bits-1, lxor-bits-2)
For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ n \in \mathbb{N}$ ,

(a) $ land(x[n$-$ 1:0],y,n) = land(x,y[n$-$ 1:0],n) = land(x,y,n)$
(b) $ lior(x[n$-$ 1:0],y,n) = lior(x,y[n$-$ 1:0],n) = lior(x,y,n)$
(c) $ lxor(x[n$-$ 1:0],y,n) = lxor(x,y[n$-$ 1:0],n) = lxor(x,y,n)$ .

PROOF: We present the proof of (a); (b) and (c) are similar.

The case $ n=0$ follows from Lemma 3.2.1. Let $ n>0$ and proceed by induction, assuming that the equation holds with $ n$ replaced by $ n-1$ . Then by Lemma 2.2.14,

$\displaystyle land(\lfloor x[n$-$\displaystyle 1:0]/2 \rfloor, \lfloor y/2 \rfloor,n-1)$ $\displaystyle =$ $\displaystyle land(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0],\lfloor y/2 \rfloor,n-1)$  
  $\displaystyle =$ $\displaystyle land(\lfloor x/2 \rfloor,\lfloor y/2 \rfloor,n-1).$  

It follows from Definition 3.2.1 that

$\displaystyle land(x[n$-$\displaystyle 1:0],y,n) = land(x,y,n).$

It may be similarly shown that $ y$ may be replaced by $ y[n$-$ 1:0]$ . 


The third argument determines the width of the result.

  (land-bvecp,lior-bvecp,lxor-bvecp)
For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ n \in \mathbb{N}$ , the following are all n-bit vectors:

(a) $ land(x,y,n)$
(b) $ lior(x,y,n)$
(c) $ lxor(x,y,n)$ .

PROOF: We present the proof of (a); (b) and (c) are similar.

The case $ n=0$ follows from Lemma 3.2.1. Let $ n>0$ and proceed by induction, assuming that the equation holds with $ n$ replaced by $ n-1$ . Then

$\displaystyle 0 \leq land(\lfloor x/2 \rfloor, \lfloor y/2 \rfloor, n$-$\displaystyle 1) \leq 2^{n-1}-1.$

It follows from Definition 3.2.1 that

$\displaystyle 0 \leq land(x,y,n) \leq 2(2^{n-1}-1) + 1 < 2^n-1.$

Notation: For any expressions $ \phi $ , $ \psi$ , and $ \lambda$ , the size the expressions ` $ land(\phi,\psi,\lambda,)$ ' ` $ lior(\phi,\psi,\lambda,)$ ', and ` $ lxor(\phi,\psi,\lambda,)$ ' are defined to be $ \lambda$ (cf. Figure 2.4).

If $ \phi $ and $ \psi$ are expressions of sizes $ \lambda$ and $ \mu$ , respectively, then ` $ \phi \;\verb!&!\; \psi$ ', ` $ \phi \;\verb!\vert!\; \psi$ ', and ` $ \phi \;\verb!^!\; \psi$ ' are abbreviations for ` $ land(\phi,\psi,max(\lambda,\mu))$ ', ` $ lior(\phi,\psi,max(\lambda,\mu))$ ', and ` $ lior(\phi,\psi,max(\lambda,\mu))$ ' (cf. Figure 2.4).

For example, ` $ x[n$-$ 1:0] \;\verb!&!\; y[n$-$ 1:0]$ ' is an abbreviation for

$\displaystyle land(x[n$-$\displaystyle 1:0],y[n$-$\displaystyle 1:0],n)$

and according to Lemma 3.2.2, may also be used as an abbreviation for ` $ land(x,y,n)$ '.

As a consequence of Lemmas 3.1.2 and 3.2.3, it remains true that if $ \phi $ is any expression of size $ \lambda$ , then the value of $ \phi $ is a bit vector whose width is the value of $ \lambda$ .

The recursive case of each definition may be restated as follows.

  (land-def,lior-def,lxor-def) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ n \in \mathbb{N}$ , if $ n>0$ , then

(a) $ x[n$-$ 1:0] \;\verb!&!\; y[n$-$ 1:0] = 2(\lfloor x/2 \rfloor[n$-$ 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$ 2:0])+x[0] \;\verb!&!\; y[0]$
(b) $ x[n$-$ 1:0] \;\verb!\vert!\; y[n$-$ 1:0] = 2(\lfloor x/2 \rfloor[n$-$ 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$ 2:0])+x[0] \;\verb!\vert!\; y[0]$
(c) $ x[n$-$ 1:0] \;\verb!^!\; y[n$-$ 1:0] = 2(\lfloor x/2 \rfloor[n$-$ 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$ 2:0])+x[0] \;\verb!^!\; y[0]$ .

PROOF: To prove (a), we substitute 0 for $ n$ in Definition 3.2.1 and conclude that

$\displaystyle x[0] \;\verb!&!\; y[0] = \left\{\begin{array}{ll} 1 & \mbox{if $x[0] = y[0] = 1$}\\ 0 & \mbox{otherwise}. \end{array} \right.$

The desired equation is now easily seen to be a restatement of the definition. Similar reasoning applies to (b) and (c). 


The following lemma belongs to the topic of Section 3.3, but it is needed for the proofs of this section.

  (land-0, lior-0, lxor-0) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ n \in \mathbb{N}$ ,

(a) $ x[n$-$ 1:0] \;\verb!&!\; n\verb!'b!0 = 0$
(b) $ x[n$-$ 1:0] \;\verb!\vert!\; y[n$-$ 1:0] = 0 \Leftrightarrow x[n$-$ 1:0] = y[n$-$ 1:0] = 0$
(c) $ x[n$-$ 1:0] \;\verb!^!\; n\verb!'b!0 = x[n$-$ 1:0]$ .

PROOF: Each equation is trivial in the case $ n=0$ . We proceed by induction, noting first that as immediate consequences of Definitions 3.2.1, 3.2.2, and 3.2.3,

(a) $ x[0] \;\verb!&!\; 1\verb!'b!0 = 1\verb!'b!0$ ,

(b) $ x[0] \;\verb!\vert!\; x[0] = 0 \Leftrightarrow x[0] = y[0] = 0$ , and

(c) $ x[0] \;\verb!^!\; 1\verb!'b!0 = x[0]$ .

The proofs are completed by applying Lemma 3.2.4 in the case $ n>0$ :

(a) By inductive hypothesis,

$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!&!\; n\verb!'b!0$ $\displaystyle =$ $\displaystyle 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; (n-1)\verb!'b!0) + x[0] \;\verb!&!\; 1\verb!'b!0$  
  $\displaystyle =$ $\displaystyle 2 \cdot 0 + 0$  
  $\displaystyle =$ $\displaystyle 0.$  

(b) By inductive hypothesis and Lemmas 2.2.13 and 2.3.14,

$\displaystyle {x[n\mbox{-}1:0] \;\vert\; y[n\mbox{-}1:0] = 0}$
  $\displaystyle \Leftrightarrow$ $\displaystyle 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!\vert!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0]) + x[0] \;\verb!\vert!\; y[0] = 0$  
  $\displaystyle \Leftrightarrow$ $\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] = \lfloor y/2 \rfloor[n$-$\displaystyle 2:0] = x[0] = y[0] = 0$  
  $\displaystyle \Leftrightarrow$ $\displaystyle x[n$-$\displaystyle 1:1] = y[n$-$\displaystyle 1:1] = x[0] = y[0] = 0$  
  $\displaystyle \Leftrightarrow$ $\displaystyle x[n$-$\displaystyle 1:0] = y[n$-$\displaystyle 1:0] = 0.$  

(c) By inductive hypothesis and Lemmas 2.2.13 and 2.3.14,

$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!^!\; n\verb!'b!0$ $\displaystyle =$ $\displaystyle 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!^!\; (n-1)\verb!'b!0) + x[0] \;\verb!^!\; 1\verb!'b!0$  
  $\displaystyle =$ $\displaystyle 2 \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] + x[0]$  
  $\displaystyle =$ $\displaystyle 2x[n$-$\displaystyle 1:1] + x[0]$  
  $\displaystyle =$ $\displaystyle x[n$-$\displaystyle 1:0].$ $\displaystyle \medskip$  

The next six results are analogous to Lemmas 3.1.4-3.1.9 of the preceding section.

  (land-shift,lior-shift,lxor-shift) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ n \in \mathbb{N}$ , and $ k \in \mathbb{N}$ ,

(a) $ (2^kx)[n$-$ 1:0] \;\verb!&!\; (2^ky)[n$-$ 1:0] = 2^k(x[n$-$ k$-$ 1:0] \;\verb!&!\; y[n$-$ k$-$ 1:0])$
(b) $ (2^kx)[n$-$ 1:0] \;\verb!\vert!\; (2^ky)[n$-$ 1:0] = 2^k(x[n$-$ k$-$ 1:0] \;\verb!\vert!\; y[n$-$ k$-$ 1:0])$
(c) $ (2^kx)[n$-$ 1:0] \;\verb!^!\; (2^ky)[n$-$ 1:0] = 2^k(x[n$-$ k$-$ 1:0] \;\verb!^!\; y[n$-$ k$-$ 1:0])$ .

PROOF: We present the proof for (a); (b) and (c) are similar.

The proof is by induction on $ k$ . The statement is vacuous for $ k = 0$ . For $ k>0$ , since $ (2^kx)[0] = mod(2^kx,2) = 0$ , by Definition 3.2.1,

$\displaystyle (2^kx)[n$-$\displaystyle 1:0] \;\verb!&!\; (2^ky)[n$-$\displaystyle 1:0] = 2((2^{k-1}x)[n$-$\displaystyle 2:0] \;\verb!&!\; (2^{k-1}y)[n$-$\displaystyle 2:0]).$

Applying the inductive hypothesis, we may write this as

$\displaystyle 2(2^{k-1}(x[n$-$\displaystyle k$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle k$-$\displaystyle 1:0])),$

or $ 2^k(x[n$-$ k$-$ 1:0] \;\verb!&!\; y[n$-$ k$-$ 1:0])$ . 

  (fl-land,fl-lior,fl-lxor) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ n \in \mathbb{N}$ , and $ k \in \mathbb{N}$ ,

(a) $ \lfloor x/2^k \rfloor[n$-$ 1:0] \;\verb!&!\; \lfloor y/2^k \rfloor[n$-$ 1:0] = \lfloor (x[n$$ \mbox{$+$}$$ k$-$ 1:0] \;\verb!&!\; y[n$$ \mbox{$+$}$$ k$-$ 1:0])/2^k \rfloor$ ;
(b) $ \lfloor x/2^k \rfloor[n$-$ 1:0] \;\verb!\vert!\; \lfloor y/2^k \rfloor[n$-$ 1:0] = \lfloor (x[n$$ \mbox{$+$}$$ k$-$ 1:0] \;\verb!\vert!\; y[n$$ \mbox{$+$}$$ k$-$ 1:0])/2^k \rfloor$ ;
(c) $ \lfloor x/2^k \rfloor[n$-$ 1:0] \;\verb!^!\; \lfloor y/2^k \rfloor[n$-$ 1:0] = \lfloor (x[n$$ \mbox{$+$}$$ k$-$ 1:0] \;\verb!^!\; y[n$$ \mbox{$+$}$$ k$-$ 1:0])/2^k \rfloor$ .

PROOF: For the proof of (a), we note that the statement is vacuous for $ k = 0$ , and proceed by induction:

$ \lfloor x/2^k \rfloor[n$-$ 1:0] \;\verb!&!\; \lfloor y/2^k \rfloor[n$-$ 1:0]$  
    = $ \lfloor \lfloor x/2^{k-1} \rfloor/2\rfloor[n$-$ 1:0] \;\verb!&!\; \lfloor \lfloor y/2^{k-1} \rfloor/2\rfloor[n$-$ 1:0]$ (by Lemma 1.1.7)
    = $ \lfloor (\lfloor x/2^{k-1} \rfloor[n:0] \;\verb!&!\; \lfloor y/2^{k-1} \rfloor[n:0])/2\rfloor$ (by Definition 3.2.1)
    = $ \lfloor \lfloor (x[n$ +$ k$-$ 1:0] \;\verb!&!\; y[n$ +$ k$-$ 1:0])/2^{k-1} \rfloor/2\rfloor$ (by induction)
    = $ \lfloor (x[n$ +$ k$-$ 1:0] \;\verb!&!\; y[n$ +$ k$-$ 1:0])/2^k \rfloor.$ (by Lemma 1.1.7)

The proofs of (b) and (c) are similar. 

  (mod-land,mod-lior,mod-lxor) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ n \in \mathbb{N}$ , and $ k \in \mathbb{N}$ , if $ k \leq n$ , then

(a) $ mod(x[n$-$ 1:0] \;\verb!&!\; y[n$-$ 1:0],2^k) = x[k$-$ 1:0] \;\verb!&!\; y[k$-$ 1:0]$
(b) $ mod(x[n$-$ 1:0] \;\verb!\vert!\; y[n$-$ 1:0],2^k) = x[k$-$ 1:0] \;\verb!\vert!\; y[k$-$ 1:0]$
(c) $ mod(x[n$-$ 1:0] \;\verb!^!\; y[n$-$ 1:0],2^k) = x[k$-$ 1:0] \;\verb!^!\; y[k$-$ 1:0]$ .

PROOF: We present the proof for (a); (b) and (c) are similar.

The statement is vacuous for $ k = 0$ . We proceed by induction, assuming $ k>0$ . By Lemma 3.2.4, the left-hand side may be written as

$\displaystyle mod(2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0]) + z,2^k),$

which, using to Lemma 1.2.19, we may rewrite as

$\displaystyle mod(mod(2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0]),2^k) + x[0]\;\verb!&!\;y[0],2^k).$

Now by Lemma 1.2.24, the first argument of this expression is

$\displaystyle 2mod(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0],2^{k-1}).$

According to our inductive hypothesis, this reduces to

$\displaystyle 2(\lfloor x/2 \rfloor[k$-$\displaystyle 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[k$-$\displaystyle 2:0]).$

Our original expression, therefore, becomes

$\displaystyle mod(2(\lfloor x/2 \rfloor[k$-$\displaystyle 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[k$-$\displaystyle 2:0])+x[0]\;\verb!&!\;y[0],2^k).$

But, according to Definition 3.2.1, this is equivalent to

$\displaystyle mod(x[k$-$\displaystyle 1:0] \;\verb!&!\; y[k$-$\displaystyle 1:0],2^k),$

which, by Lemmas 3.2.3 and 1.2.7, is just

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

  (bits-land,bits-lior,bits-lxor)
For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ n \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ ,

(a) $ (x[n$-$ 1:0] \;\verb!&!\; y[n$-$ 1:0])[i:j] = \left\{\begin{array}{ll} x[i:j] \;\verb!&!\; y[i:j] & \mbox{if $... ...-}1:j] \;\verb!&!\; y[n\mbox{-}1:j] & \mbox{if $i \geq n$} \end{array} \right.$
(b) $ (x[n$-$ 1:0] \;\verb!\vert!\; y[n$-$ 1:0])[i:j] = \left\{\begin{array}{ll} x[i:j] \;\verb!\vert!\; y[i:j] & \mbox{... ...j] \;\verb!\vert!\; y[n\mbox{-}1:j] & \mbox{if $i \geq n$} \end{array} \right.$
(c) $ (x[n$-$ 1:0] \;\verb!^!\; y[n$-$ 1:0])[i:j] = \left\{\begin{array}{ll} x[i:j] \;\verb!^!\; y[i:j] & \mbox{if $... ...-}1:j] \;\verb!^!\; y[n\mbox{-}1:j] & \mbox{if $i \geq n$} \end{array} \right.$

PROOF: We present the proof for (a); (b) and (c) are similar.

By Definition 3.2.1,

$\displaystyle (x[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0])[i:j] = \lfloor mod(x[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0],2^{i+1})/2^j \rfloor.$

If $ i<n$ , then this reduces to

$\displaystyle \lfloor (x[i:0]\;\verb!&!\;y[i:0])/2^j\rfloor$

by Lemma 3.2.8; otherwise, Lemmas 1.2.7 and 3.2.3 yield

$\displaystyle \lfloor (x[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0])/2^j\rfloor.$

In either case, we have

$\displaystyle \lfloor (x[k:0]\;\verb!&!\;y[k:0])/2^j\rfloor,$

where $ k = min(i,n-1)$ . By Lemma 3.2.7, this is equal to

$\displaystyle \lfloor x/2^j \rfloor \;\verb!&!\; \lfloor y/2^j \rfloor,$

which, according to Lemma 2.2.13, reduces to

$\displaystyle x[k:j] \;\verb!&!\; y[k:j].$

  (bitn-land,bitn-lior,bitn-lxor)
For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ n \in \mathbb{N}$ , and $ k \in \mathbb{N}$ ,

(a) $ (x[n$-$ 1:0] \;\verb!&!\; y[n$-$ 1:0])[k] = \left\{\begin{array}{ll} x[k] \;\verb!&!\; y[k] & \mbox{if $k<n$}\\ 0 & \mbox{if $k \geq n$} \end{array} \right.$
(b) $ (x[n$-$ 1:0] \;\verb!\vert!\; y[n$-$ 1:0])[k] = \left\{\begin{array}{ll} x[k] \;\verb!\vert!\; y[k] & \mbox{if $k<n$}\\ 0 & \mbox{if $k \geq n$} \end{array} \right.$
(c) $ (x[n$-$ 1:0] \;\verb!^!\; y[n$-$ 1:0])[k] = \left\{\begin{array}{ll} x[k] \;\verb!^!\; y[k] & \mbox{if $k<n$}\\ 0 & \mbox{if $k \geq n$} \end{array} \right.$

PROOF: This is the case of Lemma 3.1.7 with $ i=j=k$ . 

  (land-cat,lior-cat,lxor-cat)
For all $ x_1 \in \mathbb{N}$ , $ y_1 \in \mathbb{N}$ , $ x_2 \in \mathbb{N}$ , $ y_2 \in \mathbb{N}$ , $ m \in \mathbb{N}$ , and $ n \in \mathbb{N}$ ,

(a) $ \{x_1[m$-$ 1:0],y_1[n$-$ 1:0]\} \;\verb!&!\; \{x_2[m$-$ 1:0],y_2[n$-$ 1:0]\}$
            = $ \{x_1[m$-$ 1:0] \;\verb!&!\; x_2[m$-$ 1:0],y_1[n$-$ 1:0] \;\verb!&!\; y_2[n$-$ 1:0]\}$

(b) $ \{x_1[m$-$ 1:0],y_1[n$-$ 1:0]\} \;\verb!\vert!\; \{x_2[m$-$ 1:0],y_2[n$-$ 1:0]\}$
            = $ \{x_1[m$-$ 1:0] \;\verb!\vert!\; x_2[m$-$ 1:0],y_1[n$-$ 1:0] \;\verb!\vert!\; y_2[n$-$ 1:0]\}$

(c) $ \{x_1[m$-$ 1:0],y_1[n$-$ 1:0]\} \;\verb!^!\; \{x_2[m$-$ 1:0],y_2[n$-$ 1:0]\}$
            = $ \{x_1[m$-$ 1:0] \;\verb!^!\; x_2[m$-$ 1:0],y_1[n$-$ 1:0] \;\verb!^!\; y_2[n$-$ 1:0]\}$

PROOF: We present the proof for (a); (b) and (c) are similar.

Let $ C = \{x_1[m$-$ 1:0],y_1[n$-$ 1:0]\} \;\verb!&!\; \{x_2[m$-$ 1:0],y_2[n$-$ 1:0]\}$ . By Lemmas 3.2.8 and 2.4.13,

$\displaystyle {mod(C,2^n)}$
  $\displaystyle =$ $\displaystyle \{x_1[m$-$\displaystyle 1:0],y_1[n$-$\displaystyle 1:0]\}[n$-$\displaystyle 1:0] \;\verb!&!\; \{x_2[m$-$\displaystyle 1:0],y_2[n$-$\displaystyle 1:0]\}[n$-$\displaystyle 1:0]$  
  $\displaystyle =$ $\displaystyle y_1[n$-$\displaystyle 1:0] \;\verb!&!\; y_2[n$-$\displaystyle 1:0].$  

By Lemma 3.2.7,

$\displaystyle \lfloor C/2^n \rfloor = \lfloor \{x_1[m$-$\displaystyle 1:0],y_1[n$-$\displaystyle 1:0]\}/2^n\rfloor \;\verb!&!\; \lfloor \{x_2[m$-$\displaystyle 1:0],y_2[n$-$\displaystyle 1:0]\}/2^n\rfloor,$

where, by Definition 2.4.1 and the properties of the floor,
$\displaystyle \lfloor \{x_i[m$-$\displaystyle 1:0],y_i[n$-$\displaystyle 1:0]\}/2^n\rfloor$ $\displaystyle =$ $\displaystyle \lfloor (2^nx_i[m$-$\displaystyle 1:0]+y_i[n$-$\displaystyle 1:0])/2^n\rfloor$  
  $\displaystyle =$ $\displaystyle x_i[m$-$\displaystyle 1:0]+\lfloor y_i[n$-$\displaystyle 1:0]/2^n\rfloor$  
  $\displaystyle =$ $\displaystyle x_i[m$-$\displaystyle 1:0].$  

Thus,

$\displaystyle \lfloor C/2^n \rfloor = x_1[m$-$\displaystyle 1:0] \;\verb!&!\; x_2[m$-$\displaystyle 1:0].$

Finally, by Definitions 1.2.1 and 2.4.1,
$\displaystyle C$ $\displaystyle =$ $\displaystyle \lfloor C/2^n \rfloor 2^n + mod(C,2^n)$  
  $\displaystyle =$ $\displaystyle 2^n(x_1[m$-$\displaystyle 1:0] \;\verb!&!\; x_2[m$-$\displaystyle 1:0]) + y_1[m$-$\displaystyle 1:0] \;\verb!&!\; y_2[m$-$\displaystyle 1:0])$  
  $\displaystyle =$ $\displaystyle \{x_1[m$-$\displaystyle 1:0] \;\verb!&!\; x_2[m$-$\displaystyle 1:0],y_1[n$-$\displaystyle 1:0] \;\verb!&!\; y_2[n$-$\displaystyle 1:0]\}.$  

Results of the binary operations are ordered as follows.

  (land-bnd,lior-bnd,lxor-bnd)
For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ z \in \mathbb{N}$ , and $ n \in \mathbb{N}$ ,

(a) $ x[n$-$ 1:0] \;\verb!&!\; y[n$-$ 1:0] \leq x[n$-$ 1:0]$ ;
(b) $ x[n$-$ 1:0] \leq x[n$-$ 1:0] \;\verb!\vert!\; y[n$-$ 1:0]$ ;
(c) $ (x[n$-$ 1:0] \;\verb!^!\; y[n$-$ 1:0] \leq x[n$-$ 1:0] \;\verb!\vert!\; y[n$-$ 1:0]$ .

PROOF: We shall present an inductive proof of (a). For $ n=0$ , the statement is trivial. For $ n>0$ ,

$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0] = 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&! \lfloor y/2 \rfloor[n$-$\displaystyle 2:0]) + x[0] \;\verb!&! y[0].$

But clearly, $ x[0] \;\verb!&! y[0] \leq x[0]$ , and hence, by inductive hypothesis,

$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0] \leq 2 \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] + x[0],$

but by Lemmas 2.2.13 and 2.3.14,

$\displaystyle 2 \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] + x[0] = 2x[n$-$\displaystyle 1:1] + x[0] = x[n$-$\displaystyle 1:0].$

The proofs of (b) and (c) are similar, requiring the observations that

$\displaystyle x[0] \;\verb!\vert! y[0] \geq x[0]$

and

$\displaystyle x[0] \;\verb!\vert! y[0] \geq x[0] \;\verb!^! y[0],$

respectively. 


  (lior-plus) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ n \in \mathbb{N}$ , if

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

then

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

PROOF: By Lemma 3.2.4,

$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!\vert!\; y[n$-$\displaystyle 1:0] = 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!\vert!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0])+x[0] \;\verb!\vert!\; y[0].$

and by Lemma 3.2.7,

$\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0] = \lfloor (x[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0])/2 \rfloor = 0.$

Therefore, applying induction, we may assume that

$\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!\vert!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0] = \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] + \lfloor y/2 \rfloor[n$-$\displaystyle 2:0].$

It is easily verified that in the present case, $ x[0] \;\verb!\vert!\; y[0] = x[0]+y[0]$ , and hence,

$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!\vert!\; y[n$-$\displaystyle 1:0] = 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] + \lfloor y/2 \rfloor[n$-$\displaystyle 2:0]) + x[0]+y[0],$

which reduces, by Lemmas 2.2.13 and 2.3.13, to

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

We note two results pertaining to special cases of shifted arguments.

  (land-with-shifted-arg) For all $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ m \in \mathbb{N}$ , and $ n \in \mathbb{N}$ ,

$\displaystyle (2^mx)[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0] = 2^m(x[n$-$\displaystyle m$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:m]).$

PROOF: The claim is trivial for the case $ m=0$ . Assume $ m>0$ . Then by Lemma 3.2.4, the left-hand side may be written as

$\displaystyle 2(\lfloor 2^mx/2\rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0])+(2^mx)[0]\;\verb!&!\; y[0],$

or

$\displaystyle 2((2^{m-1}x)[n$-$\displaystyle 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0])+1\verb!'b!0\;\verb!&!\; y[0].$

But

$\displaystyle 1\verb!'b!0\;\verb!&!\; y[0] = 0,$

and by induction,

$\displaystyle (2^{m-1}x)[n$-$\displaystyle 2:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:0] = 2^{m-1}(x[n$-$\displaystyle m$-$\displaystyle 1:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:m$-$\displaystyle 1]).$

Thus, the original expression reduces to

$\displaystyle 2^{m-1}(x[n$-$\displaystyle m$-$\displaystyle 1:0] \;\verb!&!\; \lfloor y/2 \rfloor[n$-$\displaystyle 2:m$-$\displaystyle 1])$

and the lemma follows from Lemma 2.2.13. 


  (lior-with-shifted-arg) Let $ m \in \mathbb{N}$ and $ n \in \mathbb{N}$ with $ m \leq n$ . Let $ x$ be an $ (n-m)$ -bit vector and $ y$ an $ m$ -bit vector. Then

$\displaystyle (2^mx)[n$-$\displaystyle 1:0] \;\verb!\vert!\; y[n$-$\displaystyle 1:0] = 2^mx + y.$

PROOF: By hypothesis, $ y[n$-$ 1:m] = 0$ , and therefore, by Lemma 3.2.14,

$\displaystyle (2^mx)[n$-$\displaystyle 1:0] \;\verb!&!\; y[n$-$\displaystyle 1:0] = 0.$

The lemma now follows from Lemma 3.2.13. 

  (land-expt, lior-expt, lxor-expt)
For all $ x \in \mathbb{N}$ , $ n \in \mathbb{N}$ , and $ k \in \mathbb{N}$ , if $ k<n$ , then

(a) $ x[n$-$ 1:0] \;\verb!&!\; (2^k)[n$-$ 1:0] = 2^kx[k]$
(b) $ x[n$-$ 1:0] \;\verb!\vert!\; (2^k)[n$-$ 1:0] = x[n$-$ 1:0]+2^k(1-x[k])$
(c) $ x[n$-$ 1:0] \;\verb!^!\; (2^k)[n$-$ 1:0] = x[n$-$ 1:0]+2^k(1-2x[k])$ .

PROOF:

(a) In the case $ k = 0$ , according to Lemma 3.2.5(a), we have

$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!&!\; n\verb!'b!1 = 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; (n-1)\verb!'b!0) + x[0] = x[0],$

and for $ k>0$ , by Lemma 2.3.10,
$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!&!\; 2^{k}[n$-$\displaystyle 1:0]$ $\displaystyle =$ $\displaystyle 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; 2^{k-1}[n$-$\displaystyle 2:0])$  
  $\displaystyle =$ $\displaystyle 2(2^{k-1}\lfloor x/2 \rfloor[k-1])$  
  $\displaystyle =$ $\displaystyle 2^{k}x[k].$  

(b) For $ k = 0$ , applying Lemmas 3.2.5(b), 2.2.13 and 2.3.14, we have

$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!\vert!\; n\verb!'b!1$ $\displaystyle =$ $\displaystyle 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!\vert!\; (n-1)\verb!'b!0) + 1$  
  $\displaystyle =$ $\displaystyle 2 \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] +1$  
  $\displaystyle =$ $\displaystyle 2x[n$-$\displaystyle 1:1] + 1$  
  $\displaystyle =$ $\displaystyle 2x[n$-$\displaystyle 1:1] + x[0]+ 1 - x[0]$  
  $\displaystyle =$ $\displaystyle x[n$-$\displaystyle 1:0] + 1-x[0],$  

and for $ k>0$ ,
$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!\vert!\; 2^{k}[n$-$\displaystyle 1:0]$ $\displaystyle =$ $\displaystyle 2\{\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!\vert!\; 2^{k-1}[n$-$\displaystyle 2:0]\}+x[0]$  
  $\displaystyle =$ $\displaystyle 2\left\{\lfloor x/2 \rfloor[n\mbox{-}2:0] + 2^{k-1}(1-\lfloor x/2 \rfloor[k-1])\right\}+x[0]$  
  $\displaystyle =$ $\displaystyle 2x[n$-$\displaystyle 1:1] + x[0] + 2^{k}(1-x[k])$  
  $\displaystyle =$ $\displaystyle x[n$-$\displaystyle 1:0]+2^{k}(1-x[k]).$  

(c) For $ k = 0$ , applying Lemmas 3.2.5(c), 2.2.13 and 2.3.14, we have

$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!^!\; n\verb!'b!1$ $\displaystyle =$ $\displaystyle 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!^!\; (n-1)\verb!'b!0) + x[0]\;\verb!^!\; 1\verb!'b!1$  
  $\displaystyle =$ $\displaystyle 2 \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] + \verb! !x[0]$  
  $\displaystyle =$ $\displaystyle 2x[n$-$\displaystyle 1:1] + 1 - x[0]$  
  $\displaystyle =$ $\displaystyle 2x[n$-$\displaystyle 1:1] + x[0]+ 1 - 2x[0]$  
  $\displaystyle =$ $\displaystyle x[n$-$\displaystyle 1:0] + 1-2x[0],$  

and for $ k>0$ ,
$\displaystyle x[n$-$\displaystyle 1:0] \;\verb!^!\; 2^{k}[n$-$\displaystyle 1:0]$ $\displaystyle =$ $\displaystyle 2\{\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!^!\; 2^{k-1}[n$-$\displaystyle 2:0]\}+x[0]\;\verb!^!\; 1\verb!'b!0$  
  $\displaystyle =$ $\displaystyle 2\left\{\lfloor x/2 \rfloor[n\mbox{-}2:0] + 2^{k-1}(1-2\lfloor x/2 \rfloor[k-1])\right\}+x[0]$  
  $\displaystyle =$ $\displaystyle 2x[n$-$\displaystyle 1:1] + x[0] + 2^{k}(1-2x[k])$  
  $\displaystyle =$ $\displaystyle x[n$-$\displaystyle 1:0]+2^{k}(1-2x[k]).$  

Next, we consider a string of 1's. Note that for $ k = 0,\ldots,n-1$ ,

$\displaystyle (2^n-1)[k]$ $\displaystyle =$ $\displaystyle mod(\lfloor (2^n-1)/2^k \rfloor,2)$  
  $\displaystyle =$ $\displaystyle mod(\lfloor 2^{n-k}-1/2^k \rfloor,2)$  
  $\displaystyle =$ $\displaystyle mod(2^{n-k}-1,2)$  
  $\displaystyle =$ $\displaystyle 1.$  

Thus, ` $ (2^n-1)[n$-$ 1:0]$ ' could be written instead as $ n\verb!'b!1\cdots 1$ .

  (land-ones, lior-ones, lxor-ones)
For all $ x \in \mathbb{N}$ and $ n \in \mathbb{N}$ ,

(a) $ x[n$-$ 1:0] \;\verb!&!\; (2^n-1)[n$-$ 1:0] = x[n$-$ 1:0]$
(b) $ x[n$-$ 1:0] \;\verb!\vert!\; (2^n-1)[n$-$ 1:0] = 2^n-1$
(c) $ x[n$-$ 1:0] \;\verb!^!\; (2^n-1)[n$-$ 1:0] = \verb! !x[n$-$ 1:0]$ .

PROOF: For each equation, the case $ n=0$ is trivial. We proceed by induction, assuming $ n>0$ :

(a) By Lemma 3.2.4, the left-hand side may be written as

$\displaystyle 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; \lfloor(2^n-1)/2\rfloor[n$-$\displaystyle 2:0]) + x[0] \;\verb!&!\; (2^n-1)[0].$

Now

$\displaystyle \lfloor(2^n-1)/2\rfloor = \lfloor 2^{n-1} -1/2\rfloor = 2^{n-1} -1,$

and hence, by induction and Lemma 2.2.13,
$\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; \lfloor(2^n-1)/2\rfloor[n$-$\displaystyle 2:0]$ $\displaystyle =$ $\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!&!\; (2^{n-1}-1)[n$-$\displaystyle 2:0]$  
  $\displaystyle =$ $\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0]$  
  $\displaystyle =$ $\displaystyle x[n$-$\displaystyle 1:1].$  

Since

$\displaystyle (2^n-1)[0] = mod(2^n-1,2) = 1,$

our original expression reduces to

$\displaystyle 2x[n$-$\displaystyle 1:1] + x[0] = x[n$-$\displaystyle 1:0]$

by Lemma 2.3.14.

(b) By Lemma 3.2.4, the left-hand side may be written as

$\displaystyle 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!\vert!\; \lfloor(2^n-1)/2\rfloor[n$-$\displaystyle 2:0]) + x[0] \;\verb!\vert!\; (2^n-1)[0].$

By induction,
$\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!\vert!\; \lfloor(2^n-1)/2\rfloor[n$-$\displaystyle 2:0]$ $\displaystyle =$ $\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!\vert!\; (2^{n-1}-1)[n$-$\displaystyle 2:0]$  
  $\displaystyle =$ $\displaystyle (2^{n-1}-1),$  

and hence, our original expression reduces to

$\displaystyle 2(2^{n-1}-1)+x[0] \;\verb!\vert!\; 1\verb!'b!1 = 2^n-2+1 = 2^n-1.$

(c) By Lemma 3.2.4, the left-hand side may be written as

$\displaystyle 2(\lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!^!\; \lfloor(2^n-1)/2\rfloor[n$-$\displaystyle 2:0]) + x[0] \;\verb!^!\; (2^n-1)[0].$

By induction and Lemma 2.2.13,
$\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!^!\; \lfloor(2^n-1)/2\rfloor[n$-$\displaystyle 2:0]$ $\displaystyle =$ $\displaystyle \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] \;\verb!^!\; (2^{n-1}-1)[n$-$\displaystyle 2:0]$  
  $\displaystyle =$ $\displaystyle \verb! !\lfloor x/2 \rfloor[n$-$\displaystyle 2:0]$  
  $\displaystyle =$ $\displaystyle 2^{n-1} - \lfloor x/2 \rfloor[n$-$\displaystyle 2:0] - 1$  
  $\displaystyle =$ $\displaystyle 2^{n-1} - x[n$-$\displaystyle 1:1] - 1$  

and by Definition 3.2.3,

$\displaystyle x[0] \;\verb!^!\; 1\verb!'b!1 = \verb! !x[0] = 1-x[0].$

Thus, our original expression reduces to
$\displaystyle 2(2^{n-1} - x[n$-$\displaystyle 1:1] - 1)+1-x[0]$ $\displaystyle =$ $\displaystyle 2^n-(2x[n$-$\displaystyle 1:1]+x[0])-1$  
  $\displaystyle =$ $\displaystyle 2^n - x[n$-$\displaystyle 1:0] - 1$  
  $\displaystyle =$ $\displaystyle \verb! !x[n$-$\displaystyle 1:0].$  

The following lemma is a generalization of Lemma 3.2.17. Since

$\displaystyle 2^i-2^j = 2^j(2^{i-j}-1),$

the expression ` $ (2^i-2^j)[n$-$ 1:0]$ ' could be written instead as

$\displaystyle \{(n-i)\verb!'b!0,(i-j)\verb!'b!1\cdots 1,j\verb!'b!0\}.$

  (land-slice,lior-slice,lxor-slice)
For all $ x \in \mathbb{N}$ , $ n \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ , if $ j \leq i \leq n$ , then

(a) $ x[n$-$ 1:0] \;\verb!&!\; (2^i$-$ 2^j)[n$-$ 1:0] = 2^jx[i$-$ 1:j]$
(b) $ x[n$-$ 1:0] \;\verb!\vert!\; (2^i$-$ 2^j)[n$-$ 1:0] = \{x[n$-$ 1:i],(2^{i-j}$-$ 1)[i$-$ j$-$ 1:0],x[j$-$ 1:0]\}$
(c) $ x[n$-$ 1:0] \;\verb!^!\; (2^i$-$ 2^j)[n$-$ 1:0] = \{x[n$-$ 1:i],\verb! !x[i$-$ 1:j],x[j$-$ 1:0]\}$ .

PROOF: By Lemma 2.4.9,

$\displaystyle x[n$-$\displaystyle 1:0] = \{x[n$-$\displaystyle 1:i], x[i$-$\displaystyle 1:j], x[j$-$\displaystyle 1:0]\},$

and since $ 2^i-2^j = 2^j(2^{i-j}-1)$ ,

$\displaystyle (2^i$-$\displaystyle 2^j)[n$-$\displaystyle 1:0] = \{(n-i)\verb!'b!0, (2^{i-j}-1)[i$-$\displaystyle j$-$\displaystyle 1:0], j\verb!'b!0\}.$

To prove (a), we apply Lemma 3.2.11 to write the left-hand side as

$\displaystyle \{x[n$-$\displaystyle 1:i]\;\verb!\vert!\; (n-i)\verb!'b!0, x[i$-$\displaystyle 1:j]\;\verb!\vert!\; (2^{i-j}-1)[i$-$\displaystyle j$-$\displaystyle 1:0], x[j$-$\displaystyle 1:0]\;\verb!\vert!\; j\verb!'b!0\}.$

The result then follows from Lemmas 3.2.5 and 3.2.17. The proofs of (b) and (c) are similar. 


Here is a special case of Lemma 3.2.18(a) that finds application in floating-point design.

  (land-slices) Let $ n \in \mathbb{N}$ , $ k \in \mathbb{N}$ , and $ \ell \in \mathbb{N}$ . If $ \ell \leq k<n$ , then

$\displaystyle (2^{n}-2^{\ell}-1)[n$-$\displaystyle 1:0] \;\verb!&!\; (2^{n} - 2^{k})[n$-$\displaystyle 1:0] = \left\{\begin{array}{ll} 2^{n}-2^{k+1} & \mbox{if $\ell = k$}\\ 2^{n}-2^{k} & \mbox{if $\ell < k$}. \end{array} \right. $

PROOF: Applying Lemmas 3.2.18, 1.1.6, and 1.1.3, we have

$\displaystyle (2^{n}-2^{\ell}-1)[n$-$\displaystyle 1:0] \;\verb!&!\; (2^{n} - 2^{k})[n$-$\displaystyle 1:0]$ $\displaystyle =$ $\displaystyle 2^{k}(2^{n}-2^{\ell}-1)[n$-$\displaystyle 1:k]$  
  $\displaystyle =$ $\displaystyle 2^{k}\lfloor (2^{n}-2^{\ell}-1)/2^{k}\rfloor$  
  $\displaystyle =$ $\displaystyle 2^{k}(2^{n-k}+\lfloor -(2^{\ell}+1)/2^{k}\rfloor)$  
  $\displaystyle =$ $\displaystyle 2^{n}-2^{k}(\lfloor 2^{\ell-k}\rfloor +1).$  

next up previous contents
Next: Algebraic Properties Up: Logical Operations Previous: Complementation   Contents
David Russinoff 2007-01-02