As the premier conference for the design and automation of electronic systems, DAC offers outstanding training, education, exhibits and superb networking opportunities for designers, researchers, tool developers and vendors.
Alan Mishchenko - Univ. of California, Berkeley, CA Luca Amaru - Synopsys, Inc., Sunnyvale, CA Mathias Soeken - École Polytechnique Fédérale de Lausanne, Switzerland Robert Brayton - Univ. of California, Berkeley, CA
Mathias Soeken - École Polytechnique Fédérale de Lausanne, Switzerland
Logic synthesis, which is the design of logic circuits and their optimization, emerged in the 1950s with pioneering work at Bell Laboratories and IBM Research. Until today logic synthesis systems enabled the widespread use of semicustom logic design by assisting designers in the development of system- and word-level models to optimized gate-level netlists. Logic synthesis algorithms have always been facing the challenge to handle designs with an extremely large number of gates. Consequently, logic synthesis and digitial design have used and led to some of the most important and intriguing algorithms and data structures in computer science; the Quine-McCluskey algorithm and binary decision diagrams are probably one of the most notable ones. Today, logic synthesis is applied to larger and more complex design problems and therefore advancing the use of algorithms and data structures in logic synthesis systems is inevitable.
In this tutorial, we present today's challenging design problems and solutions to them. The tutorial covers three parts: (i) the use of Boolean satisfiability techniques to scale logic synthesis algorithms, (ii) new data structures and algorithms for delay optimization, and (iii) the application of logic synthesis in the design of quantum computers.
In the first part, it is shown how SAT solvers can be used to implement classical logic synthesis algorithms, such as technology mapping, LUT mapping, collapsing, and logic rewriting, in order to obtain better quality and higher flexibility. Key is to tightly integrate one or more SAT solvers into the algorithm and use them in an agile and reliable way. It is shown how SAT solvers can be used to generate canonical solutions. Consequently, SAT solvers can be used as a replacement for decision diagrams, retaining all their benefits but avoiding drawbacks such as memory explosion.
The second part introduces new algorithms and data structures for delay optimization, a crucial optimization criteria. An enumeration based algorithm is introduced that allows to find optimum networks for given delay constraints. Majority-inverter graphs are introduced as a logic data structure that allows for significant delay optimization due to effective algebraic rewriting techniques.
The third part illustrates an emerging application of logic synthesis. It shows how classical logic synthesis algorithms can be applied for the scalable design of quantum computers. Recent progress in fabrication makes the practical application of quantum computers a tangible prospect. And as quantum computers scale up to tackle problems in computational chemistry, machine learning, and cryptoanalysis, logic synthesis and design automation will be necessary to fully leverage the power of this emerging computational model.
This tutorial shows the state-of-the-art and research frontier of today's logic synthesis algorithms. The tutorial is supported by the use of state-of-the-art academic and industrial tools.