Exploiting satisfiability modulo theories for analog layout automation

This paper explores the use of Satisfiability Modulo Theories to handle mirror symmetry and common-centroid analog layout placement constraints. The proposed system reads the constraints and generates the corresponding equations or inequalities needed for Microsoft Z3 solver. These inequalities are resolved using quantifier free nonlinear real arithmetic theory. This theory has doubly exponential complexity in the worst case and it guarantees generating a solution if one exists. The proposed system produces multiple layouts that satisfy the constraints and allows the designer to choose the appropriate one according to designer´s experience.