Skip to main content
PRL Project

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

cite link