|
eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/6818
| Title: | Verification of Combinational Logic in Nuprl |
| Authors: | Basin, David A.
Del Vecchio, Peter |
| Keywords: | computer science
technical report |
| Issue Date: | Jun-1989 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR89-1018 |
| 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. |
| URI: | http://hdl.handle.net/1813/6818 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
