Publication

SAT-Based Exact Synthesis: Encodings, Topology Families, and Parallelism

Abstract

Exact synthesis is a versatile logic synthesis technique with applications to logic optimization, technology mapping, synthesis for emerging technologies, and cryptography. In recent years, advances in SAT solving have lead to a heightened research effort into SAT-based exact synthesis. Advantages of exact synthesis include the use of various constraints (e.g. synthesis of emerging technology circuits). However, although progress has been made, its runtime remains unpredictable. This paper identifies two key points as hurdles to further progress. First, there are open questions regarding the design and implementation of exact synthesis systems, due to the many degrees of freedom. For example, there are different CNF encodings, different symmetry breaks to choose from, and different encodings may be suitable for different domains. Second, SAT-based exact synthesis is difficult to parallelize. Indeed, this is a common drawback of logic synthesis algorithms. This paper proposes four ways to close some open questions and to reduce runtime: (i) quantifying differences between CNF encoding schemes and their impacts on runtime, (ii) demonstrating impact of symmetry breaking constraints, (iii) showing how DAG topology information can be used to decrease runtime, (iv) showing how topology information can be used to leverage parallelism.

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.