Formally Verified Synthesis of Combinational {CMOS} Circuits

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