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.

Notation: Following standard RTL syntax, we abbreviate as and as .

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

For any , thebinary representationof is

where for all . 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 ,

If , then it is easily seen that for all , and we may omit the leading zeroes in the representation of :

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