SAT Based Exact Synthesis using DAG Topology Families

SAT based exact synthesis is a powerful technique, with applications in logic optimization, technology mapping, and synthesis for emerging technologies. However, its runtime behavior can be unpredictable and slow. In this paper, we propose to add a new type of constraint based on families of DAG topologies. Such families restrict the search space considerably and let us partition the synthesis problem in a natural way. Our approach shows significant reductions in runtime as compared to state-of-the-art implementations, by up to 63.43%. Moreover, our implementation has significantly fewer timeouts compared to baseline and reference implementations, and reduces this number by up to 61%. In fact, our topology based implementation dominates the others with respect to the number of solved instances: given a runtime bound, it solves at least as many instances as any other implementation.

Published in:
2018 55Th Acm/Esda/Ieee Design Automation Conference (Dac)
Presented at:
55th ACM/ESDA/IEEE Design Automation Conference (DAC), San Francisco, CA, Jun 24-28, 2018
Jan 01 2018
New York, IEEE

 Record created 2018-12-13, last modified 2020-06-09

Rate this document:

Rate this document:
(Not yet reviewed)