Winston Haaswijk

SAT-Based Exact Multi-Level Logic Synthesis

Contacts:

Winston Jason HaaswijkPhD student, EPFL-IC-LSI

Mathias SoekenPost-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.

Optimum symmetric circuits
Optimum symmetric circuits found by an exact synthesis algorithm. Source: Donald Knuth, The Art of Computer Programming, Volume 4A.

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.

Topology families are a flexible method for developing efficient synthesis algorithms. Source: Haaswijk et al., SAT Based Exact Synthesis using DAG Topology Families, DAC’18.

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