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 floatingpoint 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 116 inputs and 107 outputs, verification by traditional methods such as case analysis would have been a practical impossibility.
CITATION STYLE
Basin, D. A., & Del Vecchio, P. (1990). Verification of combinational logic in Nuprl. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 408 LNCS, pp. 333–357). Springer Verlag. https://doi.org/10.1007/0-387-97226-9_36
Mendeley helps you to discover research relevant for your work.