Soeken, MathiasDe Micheli, GiovanniMishchenko, Alan2017-01-102017-01-102017-01-102017-03-3110.23919/DATE.2017.7927103https://infoscience.epfl.ch/handle/20.500.14299/132798WOS:000404171500155Boolean SAT solving can be used to find a minimum- size 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.Busy Man’s Synthesis: Combinational Delay Optimization With SATtext::conference output::conference proceedings::conference paper