User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Journal Article

Formally Verified Synthesis of Combinational CMOS Circuits


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

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