Formally Verified Synthesis of Combinational Circuits
by David A. Basin, Geoffrey Brown, Miriam Leeser
Integration: The International Journal of VLSI Design
- no downloads available
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.
bibTex ref: BBL91