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 , the binary representation of 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