Busy Man's Synthesis: Combinational Delay Optimization With SAT
Mathias Soeken1, Giovanni De Micheli1 and Alan Mishchenko2
1Integrated Systems Laboratory, EPFL, Lausanne, Switzerland
2Department of EECS, UC Berkeley, CA, USA
ABSTRACT
Boolean SAT solving can be used to find a minimumsize logic network for a given small Boolean function. This paper extends the SAT formulation to find a minimum-size network under delay constraints. Delay constraints are given in terms of input arrival times and the maximum depth. After integration into a depth-optimizing mapping algorithm, the proposed SAT formulation can be used to perform logic rewriting to reduce the logic depth of a network. It is shown that to be effective the logic rewriting algorithm requires (i) a fast SAT formulation and (ii) heuristics to quickly determine whether the given delay constraints are feasible for a given function. The proposed algorithm is more versatile than previous algorithms, which is confirmed by the experimental results.
