Verification of Combinational Logic in Nuprl
The work
| Authors | David A. Basin; Peter Del Vecchio |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1989 |
| Citekey | basin1989verification |
Where it appeared
| Publisher | Cornell University |
|---|---|
| Number in series | TR89-1018 |
| School | Cornell University |
Identifiers
| handle | 1813/6818 |
|---|
Access
| Landing page | https://hdl.handle.net/1813/6818 |
|---|
Related
| Distinct from | basin1991formally Two different works from the same Cornell group, easily conflated: both are Basin, both are transistor-level CMOS verification, both are 1989-1991. This is TR 89-1018, Basin and Del Vecchio, a 26-page case study that *verifies* one circuit -- the MAEC, front end of a floating-point adder/subtractor, 5459 transistors -- against a hand-written switch model. basin1991formally is Basin, Brown and Leeser in Integration 11(3):235--250, which turns that model into verified *synthesis*: transformation rules, proven correct with respect to a formal transistor model, that generate CMOS implementations from logical specifications. Brown and Leeser are thanked in this TR's acknowledgements for proof-reading it, so the TR is the earlier and narrower of the two, not a preprint of it. |
|---|
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.
A copy is held
pdf, 1.8 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-15 18:04 UTC |
| Approved by | a person 2026-09-15 18:06 UTC |
Cite it as
@techreport{basin1989verification,
title = {Verification of Combinational Logic in Nuprl},
author = {David A. Basin and Peter Del Vecchio},
year = {1989},
publisher = {Cornell University},
school = {Cornell University},
}
This record lives at https://refs.drheap.org/basin1989verification/ and will keep doing so.