2.4  Concatenation

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

$\displaystyle (\beta_{m-1}\cdots\beta_0\gamma_{n-1}\cdots\gamma_0)_2.$

This notion is generalized by the following function, which takes a list of bit vectors and widths, coerces each bit vector to its associated width, and concatenates the results:

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

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

This construction is extended recursively to $ 2k$ arguments for arbitrary $ k$:

$\displaystyle cat(x_1, n_1, x_2, n_2, \ldots, x_k, n_k) = cat(x_1, n_1, cat(x_2, n_2, \ldots, x_k, n_k), n_2 + \ldots + n_k),
$

where $ x_i \in \mathbb{Z}$ and $ n_i \in \mathbb{N}$ for $ i=1,\ldots,k$.

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

PROOF: By Lemma 2.2.1, $ x[m-1:0] < 2^m$ and $ y[n-1:0] < 2^n$. 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.13,

$\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.13,

$\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.15,

$\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.23,

$\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).$  

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 has an associated (explicit or implicit) 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 applications of the functions bits, bitn, and cat:

$ \blacktriangleright$ The size of the expression $ \phi[i:j$ is $ i+j-1$.

$ \blacktriangleright$ The size of the expression $ \phi[i]$ is 1.

$ \blacktriangleright$ The size of the expression $ cat(\phi_1,n_1,\ldots,\phi_k,n_k)$ is $ n_1 + \ldots + n_k$.
the basic property of sized expressions is that if $ \phi$ is an expression of size $ n$, then the value of $ \phi$ is a bit vector of width $ n$.

We adopt the following notation for the concatenation of bit vectors that are represented by sized expressions: If $ \phi_i$ is an expression of size $ n_i$ for $ i-1,\ldots,k$, then $ \{\phi_1, \phi_k\}$ is an abbreviation for $ cat(\phi,\lambda,\phi_k, n_k)$.

If the value of an expression $ \phi$ is a bit vector of width $ n$, then $ n\verb!'!\phi$ is an abbreviation for $ \phi[n-1:0]$, and therefore is an expression of size $ n$. (This is standard RTL syntax in the case where $ \phi$ is a constant.) Furthermore, in specifying a bit vector of width $ n$, we shall write $ \verb!b!\beta_1\ldots\beta_n$ as an alternative to $ (\beta_1\ldots\beta_n)_2$.

Thus, for example,

$\displaystyle \{x[8:0], 5\verb!'b!10111, y[3]\} = cat(x, 9, 23, 5, y[3], 1).
$

If the value $ \phi$ is a single bit, then we may simply write $ \phi$ as an abbreviation for $ 1\verb!'!\phi$.

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 $ y[n-1:0] = k[n-1:0]$ and $ x[m-1:0] = k[n+m-1:n]$.

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.15, and 1.2.6,

$\displaystyle k[n-1:0] = k \bmod 2^n = y[n-1:0] \bmod 2^n = y[n-1:0].$

Now by Definition 2.0.1,

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

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

$\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.4, 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 $ x_1[m-1:0] = x_2[m-1:0]_2$ and $ y_1[n-1:0]_1 = y_2[n-1:0]$.

The following is essentially a restatement of Lemma 2.2.22, 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 $ j = k+1$, 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.22, 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 $ j = k+1$, 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 $ j = k+1$, 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 $ i=j+1$, 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, $ k$ is an $ (m+n)$-bit vector. Our goal is to compute $ k[i:j]$. We consider five cases as suggested by the lemma statement, each of which involves two or more applications of Lemma 2.2.23.



Case 1: $ n>i$

By Lemma 2.2.23,

$\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.23,

$\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 $ k[i:m+n] = 0$ by Lemma 2.2.14 and hence

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

by Lemma 2.4.4. Now by Lemma 2.2.23,
$\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.23,
$\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 $ n>j$

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, $ k[n-1:j] = y[n-1:j].$ By Lemma 2.2.14, $ k[i:m+n] = 0$, 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 $ i=j$. Note that for the third case, the lemma gives $ x[m-1:i-n]$, but since $ i>n+m$, i.e., $ i-n >m-1$, this reduces to 0 by Lemma 2.2.13


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,...
...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 $ n > 0$,

$\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 $ x$ 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 $ n = 0$. Using induction, let $ n > 0$ 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: The size the expression ` $ mulcat(\ell,n,\phi)$' is defined to be $ \ell n$. As a consequence of Lemma 2.4.16, the basic property of sized expressions is preserved.

If $ \phi$ is an expression of size $ \ell$, then $ \{n \{\phi\}\}$ is an abbreviation for $ mulcat(\ell,n,\phi)$.

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

Note that the definition of mulcat 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!'!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!'0!\}\} = 0$.

PROOF: By induction and Lemma 2.4.3,

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

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

PROOF: By induction,

$\displaystyle \{n \{1\verb!'!1\}\}$ $\displaystyle =$ $\displaystyle \{\{n-1 \{1\verb!'!1\}\},1\verb!'!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.$  

  (bitn-mulcat-1) For all $ x \in \mathbb{N}$, $ n \in \mathbb{N}$, and $ m \in \mathbb{N}$, $ m \in \mathbb{N}$, if $ m < n$, then

$\displaystyle \{n \{x[0]\}\}[m] = x[0].$

PROOF: If $ n=1$, then by Lemmas 2.4.17 and 2.3.7,

$\displaystyle \{n \{x[0]\}\}[m] = \{1 \{x[0]\}\}[0] = x[0][0] = x[0].$

If $ n>1$, then

$\displaystyle \{n \{x[0]\}\}[m] = \{\{n-1 \{x[0]\}\},x[0]\}[m]$

and we invoke Lemma 2.4.14, substituting $ n-1$ for $ m$, 1 for $ n$, and $ m$ for $ i$. If $ m=0$, then the first case of the lemma applies:

$\displaystyle \{\{n-1 \{x[0]\}\},x[0]\}[0] = x[0][0] = x[0].$

If $ m>0$, then the second case of the lemma yields

$\displaystyle \{\{n-1 \{x[0]\}\},x[0]\}[m] = \{\{n-1 \{x[0]\}\}[m-1],$

and the proof is completed by induction. 

David Russinoff 2017-08-01