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 are readily available,
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: 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 optimizes resource utilization and 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 a
separate validation effort.
The book has been written with several purposes in mind. For the ACL2 user
interested in applying or extending the associated RTL library, it may be read as
a user’s manual. 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 goal is a rigorous approach to arithmetic circuit design
that is accessible and useful to architects and RTL writers.