Since the advent of computing, it has been clear that, in principle, the reliability of a computing system can be enhanced by proving that desired, precisely-stated behaviors of the system are logical consequences of the implementation of the system. We have used such an approach to analyze a combined hardware/software system.

Using the Boyer-Moore mechanical theorem-proving system we have verified the correctness of a "stack" of computing elements: a compiler, an assembler, and a microprocessor. This entire stack, from gates and latches up to "customer spec," has been carried out in a single mathematical logic and all proofs have been mechanically checked. In addition, all the mechanical proofs are rigorously tied together: the assumptions of one level are the proved consequences of the level below.

In this talk we summarize this effort and make note of our use of this approach for commercial products. We have used this approach to verify properties of the AMD K5 divide algorithm and the Motorola CAP digital signal processor. We are currently applying this approach to future IBM products.