Generalized SAT-sweeping for post-mapping optimization

Modern synthesis flows apply a series of technology independent optimization steps followed by mapping algorithms which bind the optimized network to a specific technology library. As the exact solution of the mapping problem is computationally intractable, algorithms used in practice use heuristic, typically tree-based approaches. The application of these algorithms results in mapped but suboptimal networks. In this work, we present a novel, efficient, and effective optimization algorithm for mapped networks which can be considered a generalization of SAT-sweeping. Our algorithm searches for alternative, more efficient implementations of each net in the network. Candidate support nets for reimplementation are selected using simulation signatures and verified using Boolean satisfiability. We report experimental results on the quality of our algorithm obtained from an implementation of the approach using the logic synthesis system ABC.