SAT-Based Logic Synthesis

This presentation focuses on the use of Boolean satisfiability as a computation engine in solving typical problems arising in logic synthesis. In particular, a new SAT-based algorithm is presented to compute canonical irredundant sums-of-products (ISOPs) similar to Minato's well-known BDD/ZDD-based ISOP computation. In addition, a SAT-based formulation of Boolean resubstitution and Engineering Change Order (ECO) is presented. A practical advice is given on the efficient use of SAT solvers in a variety of other practical applications.

Bio: Alan Mishchenko graduated from Moscow Institute of Physics and Technology (Moscow, Russia) in 1993 with MS and received his PhD from the Glushkov Institute of Cybernetics (Kiev, Ukraine) in 1997. In 2002, he joined the EECS Department at UC Berkeley, where he is currently a full researcher. Alan’s research interests are in developing computationally efficient methods for synthesis and verification.