2  Bit Vectors

The bit vector is the fundamental RTL data type. In some contexts, it may be thought of simply as an ordered set of two-state devices. An obvious possible starting point for the formalization of RTL semantics, therefore, is the definition of a bit vector as a sequence of Boolean values. One advantage of this approach is that it allows straightforward definitions of primitive operations such as bit extraction and concatenation.

In the realm of computer arithmetic, however, a bit vector is viewed more fruitfully as the binary expansion of a integer. In our formalization, we shall identify a bit vector with the number that it so represents, i.e., we shall define a bit vector to be an integer. Consequently, the following basic operations, which form the subject of this chapter, are defined as arithmetic functions, built on the primitives of Chapter 1. The benefits of this decision will become clear in later chapters, where we explore the arithmetic of bit vectors.

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

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

Definition 2.0.2   (bitn) For all $ x \in \mathbb{Z}$ and $ n \in \mathbb{Z}$,

$\displaystyle bitn(x,n) = x[n:n].$

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

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

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

For any $ x \in \mathbb{Z}$, the binary representation of $ x$ is

$\displaystyle x = (\ldots b_2 b_1b_0)_2,

where $ b_i = x[i]$ for all $ i \in \mathbb{N}$. We may omit the subscript 2 when the intention is clear.

In the sequel, we shall extend this notation to non-integral floating-point numbers: for $ k \in \mathbb{N}$,

$\displaystyle 2^{-k}x = (\ldots b_k.b_{k-1} \ldots b_1b_0)_2.

If $ 0 \leq x < 2^n$, then it is easily seen that $ x[k] = 0$ for all $ k \geq n$, and we may omit the leading zeroes in the representation of $ x$:

$\displaystyle x = (\ldots 000b_{n-1}\ldots b_1b_0)_2 = (b_{n-1}\ldots b_1b_0)_2.

In this case, we shall say that $ x$ is an $ n$-bit vector, or a bit vector of width $ n$. We shall show (Corollary 2.3.20) that if $ x$ is an $ n$-bit vector, then

$\displaystyle \sum_{k=0}^{n-1}2^kx[k] = x.

David Russinoff 2017-08-01