next up previous contents
Next: Bit Extraction Up: Bit Vectors Previous: Recognizing Bit Vectors   Contents


Bit Slices

Let $ x$ be an $ n$ -bit vector $ \verb!b!\beta_{n-1} \cdots \beta_1\beta_0$ , and let $ n \geq i \geq j \geq 0$ . The bit slice operator $ bits(x,i,j)$ computes the $ (i+1-j)$ -bit vector $ \verb!b!\beta_{i} \cdots \beta_j$ . It is defined formally as follows.

Definition 2.2.1   (bits) For all $ x \in \mathbb{Z}$ , $ i \in \mathbb{Z}$ , and $ j \in \mathbb{Z}$ ,

$\displaystyle bits(x,i,j) = \lfloor mod(x,2^{i+1})/2^j \rfloor.$

Notation: Following standard RTL syntax, we abbreviate ` $ bits(x,i,j)$ ' as `$ x[i:j]$ '.

For the purpose of resolving ambiguous expressions, this construction takes precedence over the basic arithmetic operators, e.g.,

$\displaystyle xy[i:j][k:\ell] = x((y[i:j])[k:\ell]).$

  (bits-bvecp) For all $ x \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ , $ x[i:j]$ is an $ (i+1-j)$ -bit vector.

PROOF: By Lemmas 1.1.1 and 1.2.3, $ bits(x,i,j) \in \mathbb{N}$ . By Lemma 1.2.4,

$\displaystyle x[i:j] = \lfloor mod(x,2^{i+1})/2^j \rfloor \leq mod(x,2^{i+1})/2^j < 2^{i+1}/2^j = 2^{i+1-j}.$

Example: Let $ x = 93 = \verb!b!1011101$ . Then

$\displaystyle x[4:2] = \lfloor mod(x,2^5)/2^2 \rfloor = \lfloor mod(93,32)/4 \rfloor = \lfloor 29/4 \rfloor = 7 = \verb!b!111$

is a 3-bit vector and

$\displaystyle x[10:7] = \lfloor mod(93,2^{11})/2^7 \rfloor = \lfloor 93/128 \rfloor = 0 = \verb!b!0000$

is a 4-bit vector.

  (mod-bits-equal) Let $ x \in \mathbb{Z}$ , $ y \in \mathbb{Z}$ , $ i \in \mathbb{Z}$ , and $ j \in \mathbb{N}$ . If $ mod(x,2^{i+1}) = mod(y,2^{i+1})$ , then $ x[i:j] = y[i:j]$ .

PROOF: $ x[i:j] = \lfloor mod(x,2^{i+1})/2^j \rfloor = \lfloor mod(y,2^{i+1})/2^j \rfloor = y[i:j]$ . 


  (mod-bits-equal-cor) Let $ x \in \mathbb{Z}$ , $ n \in \mathbb{Z}$ , $ i \in \mathbb{Z}$ , and $ j \in \mathbb{N}$ . If $ i<n$ , then $ mod(x,2^n)[i:j] = x[i:j]$ .

PROOF: By Lemma 1.2.23, $ mod(mod(x,2^n),2^{i+1}) = mod(x,2^{i+1})$ . 


If the lower limit of a bit slice is 0, it reduces to a call to $ mod$ :

  (bits-mod) For all $ x \in \mathbb{Z}$ and $ i \in \mathbb{Z}$ ,

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

PROOF: $ x[i:0] = \lfloor mod(x,2^{i+1})/2^0 \rfloor = \lfloor mod(x,2^{i+1}) \rfloor = mod(x,2^{i+1}).$  


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

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

PROOF: By Lemmas 2.2.4 and 1.2.19,

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

By expanding $ mod$ , we may also express a bit slice in terms of the floor alone:

  (bits-mod-2) Let $ x \in \mathbb{Z}$ , $ i \in \mathbb{Z}$ , and $ j \in \mathbb{Z}$ . If $ i \geq j$ , then

$\displaystyle x[i-1:j] = \left\lfloor \frac{x}{2^j} \right\rfloor - 2^{i-j} \left\lfloor \frac{x}{2^i} \right\rfloor.$

PROOF: Applying Definitions 2.2.1 and 1.2.1 and Lemma 1.1.6, we have

$\displaystyle x[i-1:j]$ $\displaystyle =$ $\displaystyle \lfloor mod(x,2^i)/2^j \rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor \frac{x- \lfloor x/2^i \rfloor 2^i}{2^j} \right\rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor \frac{x}{2^j} - \left\lfloor \frac{x}{2^i}\right\rfloor 2^{i-j} \right\rfloor$  
  $\displaystyle =$ $\displaystyle \left\lfloor \frac{x}{2^j} \right\rfloor - 2^{i-j} \left\lfloor \frac{x}{2^i} \right\rfloor.$  

In most cases of interest, the index arguments of $ x[i:j]$ satisfy $ i \geq j \geq 0$ . However, the following two lemmas are worth noting.

  (bits-neg) For all $ x \in \mathbb{Z}$ , $ i \in \mathbb{Z}$ , and $ j \in \mathbb{Z}$ , if $ i<0$ , then

$\displaystyle x[i:j] = 0.$

PROOF: Since $ -(i+1) \geq 0$ , $ 2^{-(i+1)}x \in \mathbb{Z}$ . Applying Definition 1.2.1 and Lemma 1.1.1, we have

$\displaystyle mod(x,2^{i+1})$ $\displaystyle =$ $\displaystyle x - \lfloor x/2^{i+1} \rfloor 2^{i+1} \rfloor$  
  $\displaystyle =$ $\displaystyle x - \lfloor 2^{-(i+1)}x \rfloor 2^{i+1} \rfloor$  
  $\displaystyle =$ $\displaystyle x - 2^{-(i+1)}x 2^{i+1} \rfloor$  
  $\displaystyle =$ $\displaystyle 0.$  

  (bits-with-indices-in-the-wrong-order) Let $ x \in \mathbb{Z}$ , $ i \in \mathbb{Z}$ , and $ j \in \mathbb{Z}$ . If $ i < j$ , then $ x[i:j] = 0$ .

PROOF: By Lemma 1.2.4,

$\displaystyle mod(x,2^{i+1}) < 2^{i+1} \leq 2^j,$

and hence

$\displaystyle x[i:j] = \lfloor mod(x,2^{i+1})/2^j \rfloor \leq mod(x,2^{i+1})/2^j < 1,$

which, together with Lemma 2.2.1, implies $ x[i:j] = 0$ . 


Here is another case in which a bit slice may be reduced to 0:

  (bvecp-bits-0) Let $ x \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ j \in \mathbb{N}$ . If $ x$ is a $ j$ -bit vector, then $ x[i:j] = 0$ .

PROOF: By Lemmas 1.2.3 and 1.2.6,

$\displaystyle 0 \leq mod(x,2^{i+1}) \leq x < 2^j.$

Therefore, by Lemma 1.1.5 and Definition 1.1.1,

$\displaystyle 0 \leq x[i:j] = \lfloor mod(x,2^{i+1})/2^j \rfloor \leq mod(x,2^{i+1})/2^j < 1,$

which, together with Lemma 2.2.1, implies $ x[i:j] = 0$ . 

Corollary 2.2.10   (bits-0) For all $ i \in \mathbb{N}$ and $ j \in \mathbb{N}$ , $ 0[i:j] = 0$ .

Calls to bits may often be eliminated by means of the following.

  (bits-tail) Let $ x \in \mathbb{N}$ and $ i \in \mathbb{N}$ . If $ x$ is an $ (i+1)$ -bit vector, then $ x[i:0] = x$ .

PROOF: Since $ 0 \leq x < 2^{i+1}$ ,

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

by Lemmas 2.2.4 and 1.2.7. 

Corollary 2.2.12   (bits-drop-from-minus) Let $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , and $ i \in \mathbb{N}$ . If $ x$ and $ y$ are $ (i+1)$ -bit vectors and $ y \leq x$ , then

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

Notation: For any expressions $ \phi $ and $ \lambda$ , ` $ \lambda\verb!'!\phi$ ' is an abbreviation for the expression ` $ bits(\phi,\lambda-1,0)$ '.

This is standard RTL syntax in the case where $ \lambda$ and $ \phi $ are constants and $ \phi $ is expressed as a binary expansion consisting of at most $ \lambda$ bits, e.g.,

$\displaystyle 5\verb!'b!10111 = 23.$

But note that we are extending this notation to include arbitrary variable expressions $ \lambda$ and $ \phi $ , and to allow the width of $ \phi $ to exceed $ \lambda$ . For example, Lemma 2.2.11 may now be stated as follows.
If $ x$ is an $ (i+1)$ -bit vector, then $ (i+1)\verb!'!x = x$ .
In practice, however, we shall generally restrict our use of this construction to cases where $ \phi $ is a constant of width $ \lambda$ . 2.1

According to our next lemma, a slice of a right-shifted bit vector, $ x/2^k[i:j]$ , may always be represented as a slice of $ x$ .

  (bits-shift-down-1) For all $ x \in \mathbb{N}$ , $ i \in \mathbb{N}$ , $ j \in \mathbb{N}$ , and $ k \in \mathbb{N}$ ,

$\displaystyle \lfloor x/2^k \rfloor [i:j] = x[i+k:j+k].$

PROOF: Let $ q = \lfloor x/2^{i+k+1} \rfloor$ and $ r = mod(x,2^{i+k+1})$ , so that $ x = 2^{i+k+1}q+r$ and $ 0 \leq r < 2^{i+k+1}$ . Then

$\displaystyle \lfloor x/2^{k}\rfloor = \lfloor 2^{i+1}q+r/2^{k}\rfloor = 2^{i+1}q+ \lfloor r/2^{k}\rfloor,$

where $ \lfloor r/2^{k}\rfloor \leq r/2^{k} \leq 2^{i+1}$ . Hence,

$\displaystyle mod(\lfloor x/2^{k}\rfloor,2^{i+1}) = \lfloor r/2^{k}\rfloor$

and by Definition 2.2.1 and Lemma 1.1.7,

$\displaystyle \lfloor x/2^{k}\rfloor [i:j] = \lfloor \lfloor r/2^{k}\rfloor/2^{... ... = \lfloor r/2^{k+j}\rfloor = \lfloor mod(x,2^{i+k+1})/2^{k+j}\rfloor = x[i:j].$

  (bits-shift-down-2) For all $ x \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ k \in \mathbb{N}$ ,

$\displaystyle \lfloor x/2^k \rfloor [i:0] = \lfloor x[i+k:0]/2^k \rfloor.$

PROOF: Applying Lemma 2.2.13, Definition 2.2.1, and Lemma 2.2.4 in succession, we have

$\displaystyle \lfloor x/2^k \rfloor [i:0] = x[i+k:k] = \lfloor mod(x,2^{i+k+1})/2^k\rfloor = \lfloor x[i+k:0]/2^k \rfloor.$

  (bits-shift-up-1) For all $ x \in \mathbb{N}$ , $ i \in \mathbb{N}$ , $ j \in \mathbb{N}$ , and $ k \in \mathbb{N}$ ,

$\displaystyle (2^kx)[i:j] = x[i-k:j-k].$

PROOF: If $ k \leq i$ , then by Definition 2.2.1 and Lemma 1.2.24,

$\displaystyle (2^kx)[i:j]$ $\displaystyle =$ $\displaystyle \lfloor mod(2^kx,2^{i+1})/2^j\rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor 2^k mod(x,2^{i-k+1})/2^j\rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor mod(x,2^{i-k+1})/2^{j-k}\rfloor$  
  $\displaystyle =$ $\displaystyle x[i-k:j-k].$  

If $ i < k$ , then by Definition 2.2.1 and Corollary 1.2.10,
$\displaystyle (2^kx)[i:j]$ $\displaystyle =$ $\displaystyle \lfloor mod(2^kx,2^{i+1})/2^j\rfloor$  
  $\displaystyle =$ $\displaystyle \lfloor mod(2^{i+1}(2^{k-i-1}x),2^{i+1})/2^j\rfloor$  
  $\displaystyle =$ 0  

and $ x[i-k:j-k] = 0$ by Lemma 2.2.8. 


The next lemma provides an alternate expression for a left-shifted bit slice with lower limit 0:

  (bits-shift-up-2) For all $ x \in \mathbb{N}$ , $ i \in \mathbb{N}$ , and $ k \in \mathbb{N}$ ,

$\displaystyle 2^k x[i:0] = (2^kx)[i+k:0].$

PROOF: By Lemmas 1.2.24 and 2.2.4,

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

We note two cases in which a bit slice of $ x+2^ky$ can be simplified.

  (bits-plus-mult-1) Let $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ m \in \mathbb{N}$ , $ n \in \mathbb{N}$ , and $ k \in \mathbb{N}$ . If $ k \leq m$ and $ x<2^k$ , then

$\displaystyle (x+2^ky)[n:m] = y[n-k:m-k].$

PROOF: By Lemma 2.2.8, we may assume that $ n \geq m \geq k$ . Since $ 0 \leq x/2^k < 1$ ,

$\displaystyle \lfloor (x+2^ky)/2^k \rfloor = \lfloor y+2/2^k \rfloor = y.$

We apply Lemma 2.2.13, substituting $ x+2^ky$ for $ x$ , $ n-k$ for $ i$ , and $ m-k$ for $ j$ :

$\displaystyle y[n-k:m-k] = \lfloor (x+2^ky)/2^k \rfloor [n-k:m-k] = (x+2^ky)[n:m].$

  (bits-plus-mult-2) Let $ x \in \mathbb{N}$ , $ y \in \mathbb{N}$ , $ m \in \mathbb{N}$ , $ n \in \mathbb{N}$ , and $ k \in \mathbb{N}$ . If $ n < k$ , then

$\displaystyle (x+2^ky)[n:m] = x[n:m].$

PROOF: Since $ 2^ky = 2^{n+1}(2^{k-n-1}y)$ , where $ 2^{k-n-1}y \in \mathbb{Z}$ , Lemma 1.2.16 implies $ mod(x+2^ky,2^{n+1}) = mod(x,2^{n+1}).$ The lemma now follows from Lemma 2.2.2. 


Here is an important lemma that decomposes a slice into two subslices.

  (bits-plus-bits) Let $ x \in \mathbb{N}$ , $ m \in \mathbb{N}$ , $ n \in \mathbb{N}$ , and $ p \in \mathbb{N}$ . If $ m \leq p \leq n$ , then

$\displaystyle x[n:m] = 2^{p-m}x[n:p] + x[p-1:m].$

PROOF: The proof consists of three applications of Lemma 2.2.6:

$\displaystyle 2^{p-m}x[n:p] = 2^{p-m}\left(\left\lfloor \frac{x}{2^p}\right\rfloor - 2^{n+1-p}\left\lfloor \frac{x}{2^{n+1}}\right\rfloor\right),$

$\displaystyle x[p-1:m] =\left\lfloor \frac{x}{2^m}\right\rfloor - 2^{p-m}\left\lfloor \frac{x}{2^{p}}\right\rfloor,$

and hence,
$\displaystyle 2^{p-m}x[n:p] + x[p-1:m]$ $\displaystyle =$ $\displaystyle \left\lfloor \frac{x}{2^m}\right\rfloor - 2^{n+1-m}\left\lfloor \frac{x}{2^{n+1}}\right\rfloor$  
  $\displaystyle =$ $\displaystyle x[n:m].$  

Compositions of bit slices may be reduced by means of the following.

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

$\displaystyle x[i:j][k:l] = \left\{\begin{array}{ll} x[k+j:\ell+j] & \mbox{if $k \leq i-j$}\\ x[i:\ell+j] & \mbox{if $k > i-j$}. \end{array} \right.$

PROOF: By Lemma 2.2.13,

$\displaystyle x[i:j][k:\ell]$ $\displaystyle =$ $\displaystyle \lfloor x/2^{j}\rfloor [i-j:0][k:\ell]$  
  $\displaystyle =$ $\displaystyle mod(\lfloor x/2^{j}\rfloor,2^{i-j+1})[k:\ell]$  
  $\displaystyle =$ $\displaystyle \lfloor mod(mod(\lfloor x/2^{j}\rfloor,2^{i-j+1}),2^{k+1})/2^{\ell}\rfloor.$  

If $ k \leq i-j$ , then this reduces, by Corollary 1.2.23, to

$\displaystyle \lfloor mod(\lfloor x/2^{j}\rfloor,2^{k+1})/2^{\ell}\rfloor = \lfloor x/2^{j}\rfloor [k:\ell] = x[k+j:\ell+j].$

On the other hand, if $ k > i-j$ , then by Lemma 1.2.4,

$\displaystyle mod(\lfloor x/2^{j}\rfloor,2^{i-j+1}) < 2^{i-j+1} < 2^{k+1},$

and by Lemma 1.2.7, the expression reduces instead to

$\displaystyle \lfloor mod(\lfloor x/2^{j}\rfloor,2^{i-j+1})/2^{\ell}\rfloor = \lfloor x/2^{j}\rfloor [i-j:\ell] = x[i:\ell+j].$

next up previous contents
Next: Bit Extraction Up: Bit Vectors Previous: Recognizing Bit Vectors   Contents
David Russinoff 2007-01-02