Preface

It is not the purpose of this book to expound the principles of computer arithmetic algorithms, nor does it presume to offer instruction in the art of arithmetic circuit design. A variety of publications spanning these subjects have become available in recent years, including general texts as well as more specialized treatments, covering all areas of functionality and aspects of implementation. There is one relevant issue, however, that remains to be adequately addressed, namely the problem of eliminating human error from arithmetic hardware designs and establishing their ultimate correctness.

As in all areas of computer architecture, the designer of arithmetic circuitry is preoccupied with efficiency. His objective is the rapid development of logic that maximizes execution speed, guided by established practices and intuition. Subtle conceptual errors and miscalculations are accepted as inevitable, with the expectation that they will be eliminated through extensive testing. Naturally, as implementations grow in complexity through the use of increasingly sophisticated techniques, errors become more difficult to detect. Experience has shown that testing alone is insufficient to provide a satisfactory level of confidence in the functional correctness of a state-of-the-art floating-point unit.

In order to ensure the correctness of complex implementations of arithmetic operations while reducing reliance on testing, a more scrupulous approach to the design and analysis of arithmetic circuits is imperative. Loose concepts, intuition, and arguments by example must be replaced by formal development, explicit theorems, and rigorous proofs.

One problem to be addressed is the semantic gap between abstract behavioral specifications and concrete hardware models. While the design of a circuit is modeled for most purposes at the bit level, its prescribed behavior is natually expressed in terms of high-level arithmetic concepts and algorithms, It is often easier to prove the correctness of an algorithm than to demonstrate that is has been implemented accurately.

As a simple illustration, consider the addition of two numbers, and , as diagrammed below in binary notation. Let us suppose that the sum is to be truncated at the dotted line, and that the precision of is such that its least significant non-zero bit lies to the left of the line.

Rather than computing the exact value of and then extracting the truncated result, an implementation may choose to perform the truncation on instead (at the same dotted line) before adding it to . The designer, in order to convince himself of the equivalence of these two approaches, might resort to a diagram like the one above.

The next logical step would be to formulate the underlying principle in precise terms (see Lemma 5.1.16 ), explicitly identifying the necessary conditions for equivalence, and establishing its correctness by rigorous mathematical proof. The result could then be integrated into an evolving theory of computer arithmetic, and thus become available for reuse and subject to extension and generalization (e.g., Lemma 5.5.14 ) as appropriate for new applications.

Unfortunately, such results are nowhere to be found in the existing literature, which is more concerned with advanced techniques and optimizations than with their theoretical underpinnings. What prevents the organization of the essential properties of the basic data objects and operations of this domain into a theory suitable for systematic application? The foregoing example, however trivial, serves to illustrate one of the main obstacles to this objective: the modeling of data at different levels of abstraction. Numbers are naturally represented as bit vectors, which, for some purposes, may be viewed simply as strings of Boolean values. Truncation, for example, is conveniently described as the extraction of an initial segment of bits. For the purpose of analyzing arithmetic operations, on the other hand, the same data must be interpreted as abstract numbers. Although the correspondence between a rational number and its binary representation is straightforward, a rigorous proof derived from this correspondence requires more effort than an appeal to intuition based on a simple diagram. Consequently, the essential properties of bit vector arithmetic have never been formalized and compiled into a well-founded comprehensive theory. In the absence of such a theory, the designer must rediscover the basics as needed, relying on examples and intuition rather than theorems and proofs.

Nearly two centuries ago, the mathematician Niels Abel complained about a similar state of affairs in another area of mathematical endeavor [KLI72]:

It lacks so completely all plan and system that it is peculiar that so many men could have studied it. The worst is, it has never been treated stringently. There are very few theorems in [this subject] which have been demonstrated in a logically tenable manner. Everywhere one finds this miserable way of concluding from the specific to the general ....

The subject in question was the calculus, a major mathematical development with a profound impact on the sciences, but lacking a solid logical foundation. Various attempts to base it on geometry or on intuition derived from other areas of mathematics proved inadequate as the discipline grew in complexity. The result was a climate of uncertainty, controversy, and stagnation. Abel and others resolved to restore order by rebuilding the theory of calculus solely on the basis of arithmetical concepts, thereby laying the groundwork for modern mathematical analysis.

While the contemporary hardware engineer may not be susceptible to the same philosophical qualms that motivated nineteenth century mathematicians, he is certainly concerned with the “bugs” that inevitably attend undisciplined reasoning. Even if the analogy overreaches the present problem, it charts a course for its solution and sets the direction of this investigation.

Our objective is a unified mathematical theory, derived from the first principles of arithmetic, encompassing two distinct domains of discourse. The first of these, which is the subject of Part I, is the realm of register-transfer logic (RTL), comprising the primitive data types and operations on which microprocessor designs are built, i.e., bit vectors and logical operations. A critical first step is the careful formulation of these primitives in a manner consistent with our goals, which sometimes requires resistance to intuition. Thus, notwithstanding its name, we define a bit vector of width to be a natural number less than rather than a sequence of Boolean values. This decision will seem unnatural to those who are accustomed to dealing with these obects in the context of hardware description languages, but it is a critical step in the master plan of an arithmetic-based theory. As a consequence, which may also be disturbing to some, the logical operations are defined recursively rather than bit-wise.

Part II addresses the second domain of interest, the more abstract world of rational arithmetic, focusing on floating-point representations of rational numbers as bit vectors. The benefits of a rigorous approach are most evident in the chapter on floating-point rounding, which includes a variety of results that would otherwise be difficult to state or prove, especially those that relate abstract arithmetic operations on rationals to lower-level properties of bit vectors. All of the architectural rounding modes prescribed by IEEE Standard 754 are thoroughly analyzed. Moreover, since hardware implementation is of central interest, further attention is given to several other modes that are commonly used for internal computations but are not normally covered in treatises on floating-point arithmetic.

In Part III, the theory is applied to the analysis of several well known algorithms and techniques used in the implementation of elementary arithmetic operations. The purpose here is not to present a comprehensive survey of the field, but merely to demonstrate a methodology for proving the correctness of implementations, providing guidance to those who are interested in applying it further. At the time of this writing, this part consists of two chapters: one on addition, including a discussion of leading one prediction, and the other on multiplication, describing several versions of Booth encoding. Eventually, I plan to expand both of these chapters and to add a third on division and square root extraction.

This work is an outgrowth of a verification project conducted at Advanced Micro Devices, Inc. over the past ten years, the purpose of which has been to ensure the correctness of the floating-point units of the series of microprocessors developed by AMD during that period. In order to maximize confidence in the validity of our results, the ACL2 theorem prover played a central role in this effort. RTL models of the designs, written in Verilog, were automatically translated into the language of ACL2, a first order logic based on recursive functions and mathematical induction, with the syntax of LISP. Behavioral specifications of the designs were encoded in the same logic and subjected to formal proofs, which were mechanically checked by the ACL2 prover.

During the course of this project, many thousands of definitions, lemmas, and theorems--all referred to as events in the ACL2 world--were formulated and admitted to the logic by the ACL2 prover. Those events pertaining to the general principles of RTL design and computer arithmetic, i.e., not tied to a specific implementation, were collected in an evolving library for reuse in support of subsequent proofs. The current version of the library comprises approximately six hundred events. It has not only proved to be an effective tool in reducing the effort required in the verification of successive AMD processors, but has found use outside of AMD as well and is now included as a subdirectory of the standard ACL2 release.

This book is an exposition of the theory underlying the ACL2 RTL library. Here is the sense in which the word formal is used in the title: all of the definitions and results presented herein are transcriptions of mechanically checked ACL2 events. The accompanying proofs are derived from notes that were used to guide the prover interactively through this process.

The role of ACL2 in the development of the theory is evidenced in various ways, mainly in the level of rigor that is inherent in the logic and enforced by the prover. Any vague arguments, miscalculations, or missing hypotheses may be assumed to have been corrected through the mechanization process. With respect to style of presentation, the result will appeal to those readers whose thought processes most closely resemble the workings of a mechanical theorem prover; others may find it pedantic.

Special characteristics of the ACL2 logic are also apparent in the theory, especially in its emphasis on recursion and induction, which are sometimes used in unexpected ways. On the negative side, the reader will observe that the text contains no mention of real numbers, which are not represented in the basic logic (although an extension to ACL2 supporting the reals through non-standard analysis has been implemented by Reuben Gamboa[GAM99]). Thus, variables are restricted to range over the rationals, even in statements that obviously hold for the reals in general, in order to allow a strict interpretation of the claim that all results have been mechanically verified.

On the other hand, the ACL2 connection may be safely ignored by those uninterested in pursing the formal aspect of the theory. No familiarity with ACL2, LISP, or formal logic is required of (or even useful to) the reader. The exposition adheres to the most basic conventions of mathematical notation, supplemented only by several RTL constructs common to Verilog and VHDL, all of which are explicitly defined upon first use. Nor is any uncommon knowledge of mathematics presupposed. The entire contents should be accessible to a competent high school student who has been exposed to the algebra of rational numbers and the principle of mathematical induction, especially one with an assiduous capacity for detail. It should be noted, however, that repeated attempts to support this claim have been uniformly unsuccessful.

The book has been written with several purposes in mind. For the ACL2 programmer interested in applying or extending the associated RTL library, it may be read as a user's manual. Of course,the theory might also be used to guide other verification efforts, either without mechanical support or encoded in the formalism of another theorem.prover. A more ambitious hope is that arithmetic circuit designers who appreciate the value of a rigorous approach to their art may use this as a guide to reasoning about their designs. It is in this direction that the potential impact of this methodology is greatest.

This work has benefitted from a variety of contributions from my colleagues and friends. J Moore and Matt Kaufmann, the authors of ACL2, were the first to demonstrate its utility as a floating-point verification tool. What little I know about arithmetic circuits was explained to me by Mike Achenbach, Ashraf Ahmed, Kelvin Goveas, Tom Lynch, and Stuart Oberman. The Verilog-ACL2 translator, a critical component of the AMD project, was implemented by Art Flatau, Kaufmann, and Rob Sumners. The ACL2 mechanization of some of the proofs was done by Kaufmann and Eric Smith. I am also grateful to Matthew Bottkol and Cooky Goldblatt for their suggestions for improvement of an earlier manuscript. Finally, I cannot deny myself the pleasure of thanking Lin Russinoff, who designed the cover graphics and is my continual source of inspiration.

D.M.R.
Block Island, Rhode Island
August, 2005