A Pipelined Multi-core MIPS Machine pp 7-27 | Cite as

# Number Formats and Boolean Algebra

## Abstract

We begin in Sect. 2.1 with very basic definitions of intervals of integers. Because this book is meant as a building plan for formal proofs, we cannot make definitions like [1:10] = {1,2,…,10} because CAV systems don’t understand such definitions. So we replace them by fairly obvious inductive definitions. We also have to deal with the minor technical nuisance that, usually, sequence elements are numbered from left to right, but in number representations, it is much nicer to number them from right to left.

Section 2.2 on modulo arithmetic was included for several reasons. i) The notation \(mod\ k\) is overloaded: it is used to denote both the congruence *relation* modulo a number *k* or the *operation* of taking the remainder of an integer division by *k*. We prefer our readers to clearly understand this. ii) Fixed point arithmetic is modulo arithmetic, so we will clearly have to make use of it. The most important reason, however, is that iii) addition/subtraction of binary numbers and of two’s complement numbers is done by exactly the same hardware. When we get to this topic this will look completely intuitive and, therefore, there should be a very simple proof justifying this fact. Such a proof can be found in Sect. 5.1; it hinges on a simple lemma about the solution of congruence equations from this section.

The very short Sect. 2.3 on geometric sums is simply there to remind the reader of the proof of the formula for the computation of geometric sums, which is much easier to memorize than the formula itself.

Section 2.4 introduces the binary number format, presents the school method for binary addition, and proves that it works. Although this looks simple and familiar and the correctness proof of the addition algorithms is only a few lines long, the reader should treat this result with deep respect: it is probably the first time that he or she sees a proof of the fact that the addition algorithm he learned at school always works. The Old Romans, who were fabulous engineers in spite of their clumsy number systems, would have *loved* to see this proof.

Integers are represented in computers as two’s complement numbers. In Sect. 2.5, we introduce this number format and derive a small number of basic identities for such numbers. From this we derive a subtraction algorithms for binary numbers, which is quite different from the school method, and show that it works. Sections 2.2, 2.3, and 2.5 are the basis of our construction of an arithmetic unit later.

Finally, in Sect. 2.6 on Boolean Algebra, we provide a very short proof of the fundamental result that Boolean functions can be computed using Boolean expressions in disjunctive normal form. This result can serve to construct all small circuits – e.g., in the control logic – where we only specify their functionality and do not bother to specify a concrete realization. The proof is intuitive and looks simple, but it will give us the occasion to explain formally the difference between what is often called “two kinds of equations”: i) identities *e*(*x*) = *e*′(*x*) which hold for all *x* and ii) equations *e*(*x*) = *e*′(*x*) that we want to solve by determining the set of all *x* such that the equation holds. The reader will notice that this might be slightly subtle, because both kinds of equations have exactly the same form.