Next: Logical Operations Up: Bit Vectors Previous: Bit Extraction Contents

Concatenation

If $x = \verb!b!\beta_{m-1}\cdots\beta_0$ and $y = \verb!b!\gamma_{n-1}\cdots\gamma_0$ are considered as bit vectors of widths and , respectively, then the concatenation of and is the -bit vector

$\displaystyle \verb!b!\beta_{m-1}\cdots\beta_0\gamma_{n-1}\cdots\gamma_0.$

This notion is formalized as a function of four arguments:

Definition 2.4.1 (binary-cat) For all $x \in \mathbb{Z}$ , $y \in \mathbb{Z}$ , $m \in \mathbb{Z}$ , and $n \in \mathbb{Z}$ ,

$\displaystyle cat(x,m,y,n) = 2^nx[m-1:0] + y[n-1:0].$

(cat-bvecp) For all $x \in \mathbb{N}$ , $y \in \mathbb{N}$ , $m \in \mathbb{N}$ , and $n \in \mathbb{N}$ , is an -bit vector.

PROOF: By Lemma 2.2.1, and . It follows that $x[m-1:0] \leq 2^m-1$ and $y[n-1:0] \leq 2^n-1$ , and hence,

$\displaystyle cat(x,m,y,n)$	$\displaystyle =$	$\displaystyle 2^nx[m-1:0] + y[n-1:0]$
	$\displaystyle \leq$	$\displaystyle 2^n(2^m-1) + (2^n-1)$
	$\displaystyle =$	$\displaystyle 2^{n+m}-1$
	$\displaystyle <$	$\displaystyle 2^{n+m}.$

We note three trivial cases:

(cat-with-n-0) For all $x \in \mathbb{Z}$ , $y \in \mathbb{Z}$ , and $m \in \mathbb{Z}$ ,

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

PROOF: By Definition 2.4.1 and Lemma 2.2.8,

$\displaystyle cat(x,m,y,0) = 2^0x[m-1:0] + y[-1:0] = x[m-1:0].$

(cat-with-m-0) For all $x \in \mathbb{Z}$ , $y \in \mathbb{Z}$ , and $n \in \mathbb{Z}$ ,

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

PROOF: By Definition 2.4.1 and Lemma 2.2.8,

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

(cat-0) For all $y \in \mathbb{N}$ , $m \in \mathbb{N}$ , and $n \in \mathbb{N}$ ,

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

PROOF: By Definition 2.4.1 and Lemma 2.2.10,

$\displaystyle cat(0,m,y,n) = 2^n0[m-1:0] + y[n-1:0] = y[n-1:0].$

(cat-bits-1, cat-bits-2)) For all $x \in \mathbb{Z}$ , $y \in \mathbb{Z}$ , $m \in \mathbb{Z}$ , and $n \in \mathbb{Z}$ ,

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

PROOF: By Lemma 2.2.20,

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

**Figure 2.1:** Sized Expressions
$\begin{figure}\begin{center} \begin{tabular}{\vert l\vert l\vert}\hline Expressi... ...\phi,\psi,\lambda)$ & $\lambda$ \hline \end{tabular}\end{center} \end{figure}$

Notation: In standard RTL syntax, the concatenation of two bit vectors represented by expressions $\phi$ and $\psi$ is denoted by ` $\{\phi,\psi\}$ '. However, this notation depends on the following characteristic shared by conventional hardware description languages: any expression that represents a bit vector includes a reference (either explicit or implicit) to its width. In order to incorporate this notation for concatenation, as well as other elements of RTL formalism, into our informal mathematical notation, we shall identify a class of expressions that may be unambigously associated with bit vector widths. This class includes all expressions that represent applications of one of the functions bits, bitn, and cat. As we proceed, other functions will be added to this list.

For each such expression, we define another expression, called its size, as follows:

For any expressions $\phi$ , $\alpha$ , and $\beta$ , the size of the expression ` $bits(\phi,\alpha,\beta)$ ' is the expression ` $\alpha + 1 - (\beta)$ '.
For any expressions $\phi$ and $\alpha$ , the size of the expression
` $bitn(\phi,\alpha)$ ' is the expression ` '.
For any expressions $\phi$ , $\lambda$ , $\psi$ , and $\mu$ , the size of the expression ` $cat(\phi,\lambda,\psi,\mu)$ ' is the expression ` $\lambda + \mu$ '.

For example, the size of the expression ` ' is the expression ` '. But since the second expression has the same value as ` ', we may safely treat the first expression as one of size ` '.

As a matter of convenience, if $\phi$ is an expression that does not have a defined size, but the value of which is known to be a bit vector of width 1, then we may treat $\phi$ as having size 1, i.e., we may interpret $\phi$ as an abbreviation for ` $\phi[0]$ ' (i.e., for ` $bitn(\phi,0)$ '). For example, in a context in which and are known to be 1-bit vectors,

$\displaystyle \{x,y\} = \{x[0],y[0]\} = cat(x,1,y,1).$

Figure 3.1 summarizes this notion of size and its extension to the various types of “sized” expressions that will be introduced later in this chapter and the next.

Next, we adopt the following notation for the concatenation of bit vectors that are represented by sized expressions:

If $\phi$ and $\psi$ are expressions of sizes $\lambda$ and $\mu$ , respectively, then ` $\{\phi,\psi\}$ ' is an abbreviation for ` $cat(\phi,\lambda,\psi,\mu)$ '.
If the size of the expression $\phi_i$ is defined for $i \leq i \leq k$ , where $k \geq 3$ , then ` $\{\phi_1, \ldots, \phi_k\}$ ' is defined recursively to be an abbreviation for ` $\{\phi_1, \{\phi_2,\ldots, \phi_k\}\}$ '. (See cat.)

For example, for any expressions $\phi$ and $\psi$ and natural numbers and , ` $\phi[m-1:0]$ ' and ` $\psi[n-1:0]$ ' are expressions of sizes and , respectively. Thus,

$\displaystyle \{\phi[m-1:0],\psi[n-1:0]\}$

is an abbreviation for

$\displaystyle cat(\phi[m-1:0],m,\psi[n-1:0],n),$

which is an expression of size ` '. But note that according to Lemma 2.4.5, the expression

$\displaystyle cat(\phi,m,\psi,n)$

is represented by the same abbreviation.

Also, note that according to Lemmas 2.2.1, 2.3.3, and 2.4.1, if $\phi$ is an expression of size $\lambda$ , then the value of $\phi$ is guaranteed to be a bit vector whose width is the value of $\lambda$ . As we introduce other abbreviations and extend our notion of size to other types of expressions, we shall ensure that this property is preserved.

A complete list of abbreviations based on RTL syntax is contained in Figure 3.2.

**Figure:** Abbreviations ( $\hat{\phi}$ denotes the size of $\phi$ )
$\begin{figure}\begin{center} \begin{tabular}{\vert l\vert l\vert}\hline Abbrevia... ...psi,max(\hat{\phi},\hat{\psi}))$ \hline \end{tabular}\end{center} \end{figure}$

Example: Since ` ', ` ', and ` ' are expressions of sizes ` ', ` ', and ` ', respectively, according Lemma 2.4.1, we may write

$\displaystyle {\{x[m\mbox{-}1:0],y[n\mbox{-}1:0],z[p\mbox{-}1]\}}$
	$\displaystyle =$	$\displaystyle \{x[m$ - $\displaystyle 1:0],\{y[n$ - $\displaystyle 1:0],z[p$ - $\displaystyle 1]\}$
	$\displaystyle =$	$\displaystyle \{x[m$ - $\displaystyle 1:0],cat(y[n$ - $\displaystyle 1:0],n,z[p$ - $\displaystyle 1:0],p)\}$
	$\displaystyle =$	$\displaystyle cat(x[m$ - $\displaystyle 1:0],m,cat(y[n$ - $\displaystyle 1:0],n,z[p$ - $\displaystyle 1],p),n+p)$
	$\displaystyle =$	$\displaystyle cat(x,m,cat(y,n,z,p),n+p).$

Concatenation is an associative operation:

(cat-associative) For all $x \in \mathbb{N}$ , $y \in \mathbb{N}$ , $z \in \mathbb{N}$ , $m \in \mathbb{N}$ , $n \in \mathbb{N}$ , and $q \in \mathbb{N}$ ,

$\displaystyle \{\{x[m-1:0],y[n-1:0]\},z[q-1:0]\} = \{x[m-1:0],\{y[n-1:0],z[q-1:0]\}\}.$

PROOF: By Definition 2.4.1,

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

By a similar process, the right side of the equation may be reduced to the same expression.

(cat-equal-constant) For all $x \in \mathbb{N}$ , $y \in \mathbb{N}$ , $m \in \mathbb{N}$ , and $n \in \mathbb{N}$ , if $k = \{x[m-1:0],y[n-1:0]\}$ , then and .

PROOF: By Definition 2.4.1, we have

$\displaystyle k = 2^nx[m-1:0] + y[n-1:0],$

where $0 \leq y[n-1:0] < 2^n$ by Lemma 2.2.1. Thus, by Lemmas 2.2.4, 1.2.16, and 1.2.7,

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

Now by Definition 2.2.1,

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

But Lemma 2.4.1 yields $k < 2^{n+m}$ and hence, by Lemma 1.2.7,

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

Finally, by Lemma 1.1.6, this reduces to

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

Corollary 2.4.8 (cat-equal-rewrite) For all $x_1 \in \mathbb{N}$ , $x_2 \in \mathbb{N}$ , $y_1 \in \mathbb{N}$ , $y_2 \in \mathbb{N}$ , $m \in \mathbb{N}$ , and $n \in \mathbb{N}$ , if

$\displaystyle \{x_1[m-1:0],y_1[n-1:0]\} = \{x_2[m-1:0],y_2[n-1:0]\},$

then and .

The following is essentially a restatement of Lemma 2.2.19, but is an important rewrite rule for concatenating adjacent bit slices:

(cat-bits-bits) Let $x \in \mathbb{N}$ , $i \in \mathbb{N}$ , $j \in \mathbb{N}$ , $k \in \mathbb{N}$ , and $\ell \in \mathbb{N}$ . If $i \geq j$ , $k \geq \ell$ , and , then

$\displaystyle \{x[i:j],x[k:\ell]\} = x[i:\ell].$

PROOF: By Definition 2.4.1,

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

but by Lemma 2.2.19, this reduces to $x[i:\ell]$ .

We list three special cases of Lemma 2.4.9:

Corollary 2.4.10 (cat-bitn-bits) Let $x \in \mathbb{N}$ , $j \in \mathbb{N}$ , $k \in \mathbb{N}$ , and $\ell \in \mathbb{N}$ . If $k \geq \ell$ and , then

$\displaystyle \{x[j],x[k:\ell]\} = x[j:\ell].$

Corollary 2.4.11 (cat-bits-bitn) Let $x \in \mathbb{N}$ , $i \in \mathbb{N}$ , $j \in \mathbb{N}$ , and $k \in \mathbb{N}$ . If $i \geq j$ and , then

$\displaystyle \{x[i:j],x[k]\} = x[i:k].$

Corollary 2.4.12 (cat-bitn-bitn) Let $x \in \mathbb{N}$ , $i \in \mathbb{N}$ , and $j \in \mathbb{N}$ . If , then

$\displaystyle \{x[i],x[j]\} = x[i:j].$

The next lemma is a formula for extracting a bit slice from a concatenation:

(bits-cat) For all $x \in \mathbb{N}$ , $y \in \mathbb{N}$ , $z \in \mathbb{N}$ , $m \in \mathbb{N}$ , and $i \in \mathbb{N}$ , and $j \in \mathbb{N}$ , if $i \geq j$ , then

$\displaystyle {\{x[m-1:0],y[n-1:0]\}[i:j]}$
	$\displaystyle =$	$\displaystyle \left\{\begin{array}{ll} y[i:j] & \mbox{if $n>i$}\\ x[i-n:j-n] &... ... \{x[m-1:0],y[n-1:j]\} & \mbox{if $i \geq n+m$ and $n>j$}. \end{array} \right.$

PROOF: Let $k = \{x[m-1:0],y[n-1:0]\}$ . By Lemma 2.4.7,

$\displaystyle y[n-1:0] = k[n-1:0]$

and

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

and by Lemma 2.4.1,

is an

-bit vector. Our goal is to compute

. We consider five cases as suggested by the lemma statement, each of which involves two or more applications of Lemma 2.2.20.

Case 1:

By Lemma 2.2.20,

$\displaystyle k[i:j] = k[n-1:0][i:j] = y[n-1:0][i:j] = y[i:j].$

Case 2: $m+n>i \geq j \geq n$

By Lemma 2.2.20,

$\displaystyle k[i:j]$	$\displaystyle =$	$\displaystyle k[m+n-1:n][i-n:j-n]$
	$\displaystyle =$	$\displaystyle x[m-1:0][i-n:j-n]$
	$\displaystyle =$	$\displaystyle x[i-n:j-n].$

Case 3: $i \geq m+n$ and $j \geq n$

By Lemma 2.4.9,

$\displaystyle k[i:j] = \{k[i:m+n],k[m+n-1:j]\}.$

But

by Lemma 2.2.9 and hence

$\displaystyle k[i:j] = k[m+n-1:j]$

by Lemma 2.4.4. Now by Lemma 2.2.20,

$\displaystyle k[m+n-1:j]$	$\displaystyle =$	$\displaystyle k[m+n-1:n][m-1:j-n]$
	$\displaystyle =$	$\displaystyle x[m-1:0][m-1:j-n]$
	$\displaystyle =$	$\displaystyle x[m-1:j-n].$

Case 4: $m+n >i \geq n > j$

By Lemma 2.4.9,

$\displaystyle k[i:j] = \{k[i:n],k[n-1:j]\}.$

But by Lemma 2.2.20,

$\displaystyle k[i:n]$	$\displaystyle =$	$\displaystyle k[m+n-1:n][i-n:0]$
	$\displaystyle =$	$\displaystyle x[m-1:0][i-n:0]$
	$\displaystyle =$	$\displaystyle x[i-n:0]$

and

$\displaystyle k[n-1:j]$	$\displaystyle =$	$\displaystyle k[n-1:0][n-1:j]$
	$\displaystyle =$	$\displaystyle y[n-1:0][n-1:j]$
	$\displaystyle =$	$\displaystyle y[n-1:j].$

Case 5: $i \geq n+m$ and

By Lemma 2.4.9,

$\displaystyle k[i:j] = \{k[i:m+n],k[m+n-1:n],k[n-1:j]\}.$

As in Case 4,

By Lemma 2.2.9,

, and hence by Lemma 2.4.4,

$\displaystyle k[i:j] = \{k[m+n-1:n],k[n-1:j]\} = \{x[m-1:0],y[n-1:j]\}.$

(bitn-cat) For all $x \in \mathbb{N}$ , $y \in \mathbb{N}$ , $z \in \mathbb{N}$ , $m \in \mathbb{N}$ , and $i \in \mathbb{N}$ ,

$\displaystyle \{x[m-1:0],y[n-1:0]\}[i] = \left\{\begin{array}{ll} y[i] & \mbox{... ...] & \mbox{if $n \leq i<m+n$}\\ 0 & \mbox{if $n+m \leq i$}. \end{array} \right.$

PROOF: The cases listed correspond to the first three cases of Lemma 2.4.13 with . Note that for the third case, the lemma gives , but since , i.e., , this reduces to 0 by Lemma 2.2.8.

The function mulcat concatenates several copies of a bit vector:

Definition 2.4.2 (mulcat) For all $x \in \mathbb{N}$ , $n \in \mathbb{N}$ , and $\ell \in \mathbb{N}$ ,

$\displaystyle mulcat(\ell,n,x) = \left\{\begin{array}{ll} cat(mulcat(\ell,n-1,x),\ell(n-1),x,\ell) & \mbox{if $n>0$}\\ 0 & \mbox{if $n=0$}. \end{array} \right.$

(mulcat-bits) For all $x \in \mathbb{Z}$ , $\ell \in \mathbb{Z}$ , and $n \in \mathbb{Z}$ ,

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

PROOF: This is proved by induction, using Lemma 2.4.5. For ,

$\displaystyle mulcat(\ell,n,x)$	$\displaystyle =$	$\displaystyle cat(mulcat(\ell,n-1,x),\ell(n-1),x,\ell)$
	$\displaystyle =$	$\displaystyle cat(mulcat(\ell,n-1,x[\ell-1:0]),\ell(n-1),x[\ell-1:0],\ell)$
	$\displaystyle =$	$\displaystyle mulcat(\ell,n,x[\ell-1:0]).$

(mulcat-bvecp) If is an $\ell$ -bit vector and $n \in \mathbb{N}$ , then

$\displaystyle mulcat(\ell,n,x)$

is an $n\ell$ -bit vector.

PROOF: The claim is trivial for . Using induction, let and assume that $mulcat(\ell,n-1,x)$ is a bit vector of width $(n-1)\ell$ . Then by Lemma 2.4.1,

$\displaystyle mulcat(\ell,n,x) = cat(mulcat(\ell,n-1,x),\ell(n-1),x,\ell)$

is a bit vector of width $\ell + (n-1)\ell = n\ell$ .

Notation: For any expressions $\lambda$ , $\phi$ , and $\tau$ , the size the expression ` $mulcat(\lambda,\phi,\tau)$ ' is defined to be the expression ` $(\lambda)(\tau)$ '. If $\lambda$ is the size of $\phi$ , then ` $\{\tau \{\phi\}\}$ ' is an abbreviation for ` $mulcat(\lambda,\phi,\tau)$ '.

For example, ` $\{n \{x[\ell-1:0]\}\}$ ' is an abbreviation for ` $mulcat(\ell,n-1,x[\ell-1:0])$ ' and according to Lemma 2.4.15, may also be used as an abbreviation for ` $mulcat(\ell,n-1,x)$ '.

As a consequence of Lemma 2.4.16, the basic property of sized expressions is preserved: if $\phi$ is an expression of size $\lambda$ , then the value of $\phi$ is a bit vector whose width is the value of $\lambda$ .

Note that the foregoing definition may be written as

$\displaystyle \{n \{x[\ell-1:0]\}\} = \left\{\begin{array}{ll} \{\{n\mbox{-}1 ... ...l-1:0]\}& \mbox{if $n>0$}\\ 0\verb!'b!0 & \mbox{if $n=0$}. \end{array} \right.$

We make note of several trivial identities:

(mulcat-1) For all $x \in \mathbb{N}$ and $\ell \in \mathbb{N}$ ,

$\displaystyle \{1 \{x[\ell-1:0]\}\} = x[\ell-1:0].$

PROOF: By Lemma 2.4.3,

$\displaystyle \{1 \{x[\ell-1:0]\}\}$	$\displaystyle =$	$\displaystyle \{\{0 \{x[\ell-1:0]\}\},x[\ell-1:0]\}$
	$\displaystyle =$	$\displaystyle cat(0,0,x[\ell-1:0],\ell)$
	$\displaystyle =$	$\displaystyle x[\ell-1:0].$

(mulcat-0) For all $n \in \mathbb{N}$ and $\ell \in \mathbb{N}$ , $\{n \{\ell\verb!'b0!\}\} = 0$ .

PROOF: By induction and Lemma 2.4.3,

$\displaystyle \{n \{\ell\verb!'b0!\}\}$	$\displaystyle =$	$\displaystyle \{\{n-1 \{\ell\verb!'b0!\}\},\ell\verb!'b0!\}$
	$\displaystyle =$	$\displaystyle cat(0,0,0,\ell)$
	$\displaystyle =$	$\displaystyle 0.$

(mulcat-n-1) For all $n \in \mathbb{N}$ , $\{n \{1\verb!'b!1\}\} = 2^n-1$ .

PROOF: By induction,

$\displaystyle \{n \{1\verb!'b!1\}\}$	$\displaystyle =$	$\displaystyle \{\{n-1 \{1\verb!'b!1\}\},1\verb!'b!1\}$
	$\displaystyle =$	$\displaystyle cat(2^{n-1}-1,n-1,1,1)$
	$\displaystyle =$	$\displaystyle 2^1(2^{n-1}-1)+1$
	$\displaystyle =$	$\displaystyle 2^n-1.$