EECS 298-11: CAD Seminar
Thursday, May 22, 1997, 2pm
^^^^^^^^                ^^^
Cory Hall--Hogan Room

            Incremental Methods for Logic-CAD

                  Gitanjali Swamy
                  Mentor Graphics

IC design is an iterative process; the initial specification of a
design is rarely complete and correct. The designer begins with a
preliminary and usually incorrect sketch (possibly from a previous
generation design), and iteratively refines and corrects it. Usually,
refinements are small, and there is much common information between
successive design iterations. The current genre of CAD tools do not
take into account this iterative nature of design. For each change
made to the design, the design is re-verified and re-optimized without
taking advantage of information from previous iterations, leading to
inefficient performance. We propose the paradigm of incremental
algorithms for CAD. Incremental algorithms use information from a
previous design iteration, as well as information about changes to the
design to evaluate the design efficiently. In particular, we examine
incremental algorithms for two different classes of CAD problems:
formal design verification and logic synthesis.

Formal design verification is one of the methods used in logic CAD to
validate that the design satisfies all its requirements. In this talk,
we will focus on methods for incremental formal design verification,
and talk in particular about incremental design verification using
Computational Tree logic (CTL). We prove that it is not theoretically
possible to share all common information between different CTL
specifications in less than exponential time. In light of this
argument, we propose an almost canonical representation for CTL. We
use this to construct an incremental formulation for fair-CTL model
checking and conclude with experimental evidence to demonstrate the
gains of such an approach.