Arithmetic circuits are generally modeled in hardware description languages at the register-transfer level, i.e., in terms of the flow of data between hardware registers and the logical operations performed on them. The fundamental data type of such a language is the bit vector, a sequence of binary digits.
Naturally, the notion of a bit vector is also fundamental to our theory. In Chapter 2, we present a formalization of this notion and the operations of bit extraction and bit slice and their properties. The logical operations on bit vectors are discussed in Chapter 3. All of these operations are defined in terms of the basic arithmetic functions floor and mod, which are the subject of Chapter 1.