# 2.4  Concatenation

If and are considered as bit vectors of widths and , respectively, then the concatenation of and is the -bit vector

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 , , , and ,

This construction is extended recursively to arguments for arbitrary :

where and for .

(cat-bvecp) For all , , , and , is an -bit vector.

PROOF: By Lemma 2.2.1, and . It follows that and , and hence,

We note three trivial cases:

PROOF: By Definition 2.4.1 and Lemma 2.2.13,

PROOF: By Definition 2.4.1 and Lemma 2.2.13,

PROOF: By Definition 2.4.1 and Lemma 2.2.15,

PROOF: By Lemma 2.2.23,

Notation: In standard RTL syntax, the concatenation of two bit vectors represented by expressions and is denoted by . 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:

The size of the expression is .

The size of the expression is 1.

The size of the expression is .
the basic property of sized expressions is that if is an expression of size , then the value of is a bit vector of width .

We adopt the following notation for the concatenation of bit vectors that are represented by sized expressions: If is an expression of size for , then is an abbreviation for .

If the value of an expression is a bit vector of width , then is an abbreviation for , and therefore is an expression of size . (This is standard RTL syntax in the case where is a constant.) Furthermore, in specifying a bit vector of width , we shall write as an alternative to .

Thus, for example,

If the value is a single bit, then we may simply write as an abbreviation for .

Concatenation is an associative operation:

PROOF: By Definition 2.4.1,

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

(cat-equal-constant) For all , , , and , if , then and .

PROOF: By Definition 2.4.1, we have

where by Lemma 2.2.1. Thus, by Lemmas 2.2.4, 1.2.15, and 1.2.6,

Now by Definition 2.0.1,

But Lemma 2.4.1 yields and hence, by Lemma 1.2.6,

Finally, by Lemma 1.1.4, this reduces to

Corollary 2.4.8   (cat-equal-rewrite) For all , , , , , and , if

then and .

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 , , , , and . If , , and , then

PROOF: By Definition 2.4.1,

but by Lemma 2.2.22, this reduces to

We list three special cases of Lemma 2.4.9:

Corollary 2.4.10   (cat-bitn-bits) Let , , , and . If and , then

Corollary 2.4.11   (cat-bits-bitn) Let , , , and . If and , then

Corollary 2.4.12   (cat-bitn-bitn) Let , , and . If , then

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

(bits-cat) For all , , , , and , and , if , then

PROOF: Let . By Lemma 2.4.7,

and

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.23.

Case 1:

By Lemma 2.2.23,

Case 2:

By Lemma 2.2.23,

Case 3: and

By Lemma 2.4.9,

But by Lemma 2.2.14 and hence

by Lemma 2.4.4. Now by Lemma 2.2.23,

Case 4:

By Lemma 2.4.9,

But by Lemma 2.2.23,

and

Case 5: and

By Lemma 2.4.9,

As in Case 4, By Lemma 2.2.14, , and hence by Lemma 2.4.4,

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.13

The function mulcat concatenates several copies of a bit vector:

Definition 2.4.2   (mulcat) For all , , and ,

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

(mulcat-bvecp) If is an -bit vector and , then

is an -bit vector.

PROOF: The claim is trivial for . Using induction, let and assume that is a bit vector of width . Then by Lemma 2.4.1,

is a bit vector of width

Notation: The size the expression ` ' is defined to be . As a consequence of Lemma 2.4.16, the basic property of sized expressions is preserved.

If is an expression of size , then is an abbreviation for .

For example, is an abbreviation for and according to Lemma 2.4.15, the same abbreviation may also be used for .

Note that the definition of mulcat may be written as

We make note of several trivial identities:

PROOF: By Lemma 2.4.3,

PROOF: By induction and Lemma 2.4.3,

PROOF: By induction,

PROOF: If , then by Lemmas 2.4.17 and 2.3.7,

If , then

and we invoke Lemma 2.4.14, substituting for , 1 for , and for . If , then the first case of the lemma applies:

If , then the second case of the lemma yields

and the proof is completed by induction.

David Russinoff 2017-08-01