Analog layout constraints resolution and shape function generation using Satisfiability Modulo Theories

This paper exploits one of the formal methods to generate layouts for an analog circuit, where these layouts satisfy some given analog constraints. The analog constraints are provided by the user through a text file and the used method is the Satisfiability Modulo Theories solving. After generating the layouts as valid solutions for the given constraints, the paper shows how different aspect ratios can be used in order to draw the shape function. The shape function allows the user to find optimal layouts and accordingly select one of them, given some acceptable ranges for aspect ratios, width, and height.