Formally verified synthesis of combinational CMOS circuits

Authors	David A. Basin; Geoffrey M. Brown; Miriam E. Leeser
Editors
Type	article
Year	1991
Citekey	`basin1991formally`

Published in	Integration, the VLSI Journal
Publisher	Elsevier BV
Volume	11
Issue	3
Pages	235--250

DOI	10.1016/0167-9260(91)90048-p
OpenAlex	W1994376444
ISSN	0167-9260

Landing page	https://doi.org/10.1016/0167-9260(91)90048-p

Copy	No open copy exists on any host this account may ask. The work is Elsevier's (Integration 11(3):235--250, 1991); the record's only address is the doi.org landing page, which deskr fetch classes off-spec, and sciencedirect.com is not in hosts and answers WebFetch with HTTP 403. Checked for a deposited alternative and there is none: Cornell eCommons, which does hold the companion TR 89-1018 as basin1989verification, has no tech-report version of this paper -- a search of its Computer Science Technical Reports collection for Basin returns only TR 89-1018 and Basin's 1989 dissertation (handle 1813/6863). Unpaywall, OpenAlex and Crossref were all asked via deskr enrich and none offers an open address. A 1991 Elsevier VLSI-journal article predates author self-archiving, so the likeliest routes are interlibrary loan or the ScienceDirect subscription, neither of which is an agent's to use. The companion TR is held in full and carries the same transistor model, so the corpus is not blind to the method -- only to this paper's synthesis rules.

Copy

No open copy exists on any host this account may ask. The work is Elsevier's (Integration 11(3):235--250, 1991); the record's only address is the doi.org landing page, which deskr fetch classes off-spec, and sciencedirect.com is not in hosts and answers WebFetch with HTTP 403. Checked for a deposited alternative and there is none: Cornell eCommons, which does hold the companion TR 89-1018 as basin1989verification, has no tech-report version of this paper -- a search of its Computer Science Technical Reports collection for Basin returns only TR 89-1018 and Basin's 1989 dissertation (handle 1813/6863). Unpaywall, OpenAlex and Crossref were all asked via deskr enrich and none offers an open address. A 1991 Elsevier VLSI-journal article predates author self-archiving, so the likeliest routes are interlibrary loan or the ScienceDirect subscription, neither of which is an agent's to use. The companion TR is held in full and carries the same transistor model, so the corpus is not blind to the method -- only to this paper's synthesis rules.

Distinct from	basin1989verification 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.

Distinct from

basin1989verification 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.

pdf, 914.0 kB. Not published — it may be under copyright. The facts and links here are.

How it got here	agent via crossref
Added	2026-09-15 17:55 UTC
Approved by	a person 2026-09-15 18:14 UTC

basin the-switch-or-the-curve you-cannot-patch-silicon

@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.

Formally verified synthesis of combinational CMOS circuits

The work

Where it appeared

Identifiers

Access

Settled

Related

A copy is held

How it got here

Filed under

Cite it as