Practical Exact Synthesis (Executive Session Paper)
Mathias Soeken1, Winston Haaswijk1, Eleonora Testa1, Alan Mishchenko2, Luca G. Amarù3, Robert K. Brayton2 and Giovanni De Micheli1
1Integrated Systems Laboratory, EPFL, Switzerland
2EECS, UC Berkeley, CA, USA
3Synopsys Inc., CA, USA
ABSTRACT
In this paper, we discuss recent advances in exact synthesis, considering both their efficient implementation and various applications in which they can be employed. We emphasize on solving exact synthesis through Boolean satisfiability (SAT) encodings. Different SAT encodings for exact synthesis are compared, and examined the applications to multi‐level logic synthesis, in both area and depth optimization. Another application of SAT based exact synthesis is optimization under many constraints. These constraints can, e.g., be a fixed fanout or delay constraints. Finally, we end our discussion by proposing directions for future research in exact synthesis.
