SAT-Based Exact Multi-Level Logic Synthesis
Contacts:
Winston Jason Haaswijk, PhD student, EPFL-IC-LSI
Mathias Soeken, Post-doc, EPFL-IC-LSI
Giovanni De Micheli, Professor, EPFL-IC-LSI
Motivation:
Electronic systems are ubiquitous, and their presence in the world is only increasing. Moreover, there is a trend towards increasing design complexity across multiple levels of abstraction For example, on the device level, novel technologies must make efficient use of novel logic primitives, while accounting for complex constraints such as fanout or depth restrictions. On the architectural level, there has been a trend towards complex system on a chip (SoC) designs. To ensure the continued progress of Moore’s law, researchers must find new ways of dealing with this increased complexity.
Presentation:
In recent years, there has been a lot of progress in the development of so-called SAT solvers. These are programs which specialize in solving SAT problems efficiently. Due to the NP-complete nature of SAT, fast solvers allow us to solve many problems in NP efficiently. Hence, as these solvers have become more powerful, interest in them has grown accordingly.
In the context of Electronic Design Automation (EDA), the main application of SAT has traditionally been in hardware verification and other formal tasks. We use SAT solvers as a basis for the development of new exact synthesis algorithms. Such algorithms can be guaranteed meet specifications exactly, or to prove that specifications cannot be realized (a guarantee which most heuristic algorithms do not provide). They can be used to synthesize optimum circuits, which can be applied to circuit optimization. Moreover, using SAT we can support the complex logic primitives and constraints that are imposed by novel nanotechnologies. Our goal is to analyze and extend existing algorithms, in order to push the boundaries of what is achievable with SAT-based synthesis methods.
We have recently introduced novel algorithms which take advantage of domain-specific graph topology information. By providing the SAT solver with additional constraints based on DAG topologies, we limit its search space. This reduced search space can then speed up the synthesis process. We believe this approach also lends itself to the development of parallel synthesis algorithms.
Goals:
- Analysis of SAT-based exact synthesis algorithms.
- Design of improved and more general algorithms.
- The application of exact synthesis in various EDA applications.
List of publications available here