LCS-A Leaf Cell Synthesizer Employing Formal Deduction Techniques

This paper discusses the use of formal reasoning techniques to aid in the automated structural design of leaf cells, in the more global context of VLSI circuit design. The technique supports an encapsulation of the technology-dependent aspects of a design by using appropriate formal models, and guarantees the consistency of the designs produced with respect to the functional specification and the technology model employed. The approach is illustrated by its use in the design of some leaf cells in CMOS. The role of the techniques when used in an interactive mode and in the verification of existing designs is also discussed.