Verification of Combinational Logic in Nuprl

From bibtex.

Abstract

We present a case study of hardware specification and verification in the Nuprl Proof Development System. Within Nuprl we have built a specialized environment consisting of tactics, definitions, and theorems for specifying and reasoning about hardware. Such reasoning typically consists of term-rewriting, case-analysis, induction, and arithmetic reasoning. We have built tools that provide high-level assistance for these tasks. The hardware component that we have proven is the front end of a floating-point adder/subtractor. This component, the MAEC (Mantissa Adjuster and Exponent Calculator), has 5459 transistors and has been proven down to the transistor level. As the circuit has 118 inputs and 107 outputs, verification by traditional methods such as case analysis would have been a practical impossibility.