Formally verified synthesis of combinational CMOS circuits
The work
| Authors | David A. Basin; Geoffrey M. Brown; Miriam E. Leeser |
|---|---|
| Editors | |
| Type | article |
| Year | 1991 |
| Citekey | basin1991formally |
Where it appeared
| Published in | Integration, the VLSI Journal |
|---|---|
| Publisher | Elsevier BV |
| Volume | 11 |
| Issue | 3 |
| Pages | 235--250 |
Identifiers
| DOI | 10.1016/0167-9260(91)90048-p |
|---|---|
| OpenAlex | W1994376444 |
| ISSN | 0167-9260 |
Access
| Landing page | https://doi.org/10.1016/0167-9260(91)90048-p |
|---|
Related
| Distinct from | angelo1993comparison |
|---|---|
| Distinct from | basin1989verification |
| Distinct from | bryant1987cosmos |
| Distinct from | camilleri1986hardware |
| Distinct from | ferres2025survey |
| Distinct from | fourman1986verification |
| Distinct from | fourman1991formal |
| Distinct from | gordon1983lcflsm |
| Distinct from | gordon1983proving |
| Distinct from | gordon1985why |
| Distinct from | joyce1987hardware |
| Distinct from | kumar1996formal |
| Distinct from | leeser1988reasoning |
| Distinct from | martin1986compiling |
| Distinct from | ohlinger2021involution |
From crossref.
Abstract
We present a system for simultaneously synthesizing and proving correct CMOS implementations of combinational circuits. Our system, developed within the Nuprl proof development system is based on a set of transformation rules that generate CMOS implementations from their logical specifications. Our research differs from previous work in three important ways: our rules are rigorously proven with respect to a formal transistor model, our transformation rules admit the synthesis of both pass transistor and series/parallel networks, and our implementation produces a human readable proof along with each circuit it synthesizes.
A copy is held
pdf, 914.0 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-09-15 17:55 UTC |
| Approved by | a person 2026-10-02 10:01 UTC |
Filed under
Cite it as
@article{basin1991formally,
title = {Formally verified synthesis of combinational CMOS circuits},
author = {David A. Basin and Geoffrey M. Brown and Miriam E. Leeser},
year = {1991},
journal = {Integration, the VLSI Journal},
publisher = {Elsevier BV},
volume = {11},
number = {3},
pages = {235--250},
issn = {0167-9260},
doi = {10.1016/0167-9260(91)90048-p},
}
This record lives at https://refs.drheap.org/basin1991formally/ and will keep doing so.