SMT-based placement for system-on-chip design

The utilization of System on Chips (SoCs) for short-living consumer applications has become very popular over the last decades. Because of that, more and more effort has been put into the physical design of SoCs and especially into the so-called macro placement step in order to keep the final price suitable for mass production. How to guarantee that the SoC is realized based on a minimal die area remains a challenging task. Current state-of-the-art solutions for this macro placement-problem mostly try to tackle the problem based on meta-heuristic- and genetic algorithms. However, although such methods are commonly used for macro placement, they can not guarantee that the macro placement and, therefore the die size is optimal. In this work, we are proposing the utilization of modern satisfiability solvers in order to generate optimized macro placements. To this end, we symbolically formulate the placement problem and forward it to a solver which allows us to obtain optimized solutions for the macro placement problem. In case this is not possible, search space pruning is employed which does not allow to employ the full optimization strategy anymore but still determines feasible results. We demonstrate the approach in experiments and made the resulting tool available as open-source.