English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Journal Article

Formally Verified Synthesis of Combinational CMOS Circuits

MPS-Authors
/persons/resource/persons44075

Basin,  David A.
Programming Logics, MPI for Informatics, Max Planck Society;

External Ressource
No external resources are shared
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Basin, D. A., Brown, G. M., & Leeser, M. E. (1991). Formally Verified Synthesis of Combinational CMOS Circuits. Integration: The Intern. Journal of VLSI Design, 11(3), 235-250. doi:10.1016/0167-9260(91)90048-P.


Cite as: http://hdl.handle.net/11858/00-001M-0000-001A-2593-9
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.