Pareto front analog layout placement using Satisfiability Modulo Theories
Pareto front analog layout placement using Satisfiability Modulo Theories
复制标题
使用可满足性模理论的帕累托前沿模拟布局布局
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
S. Nassar
中科院分区：
文献类型：
--
作者：
S. Saif;M. Dessouky;M. El;H. Abbas;S. Nassar
本文提出了一种模拟布局放置工具，重点是帕累托前沿生成。为了处理数量激增的模拟物理约束，提出了一种基于可满足性模理论 (SMT) 求解器的新方法。 SMT 是一个涉及检查逻辑公式对一个或多个理论的可满足性的领域。 SMT 通常经过精心调整来解决特定问题。据我们所知，这是首次使用 SMT 来解决模拟贴装问题。所提出的工具隐式生成满足给定约束的多个布局。因此，它使用户可以通过指定纵横比或从生成的形状函数的帕累托前沿选择最佳解决方案来从可行解决方案中进行选择。与大多数现有技术相比，随着物理约束数量的增加，SMT 求解器处理时间会减少。与其他技术相比，所提出的系统产生的布局具有具有竞争力的面积和运行时间。
This paper presents an analog layout placement tool with emphasis on Pareto front generation. In order to handle the exploding number of analog physical constraints, a new approach based on the use of a Satisfiability Modulo Theories (SMT) solver is suggested. SMT is an area concerned with checking the satisfiability of logical formulas over one or more theories. SMT is usually well-tuned to solve specific problems. To our knowledge, this is the first effort to use SMT to tackle analog placement. The proposed tool implicitly generates multiple layouts that fulfill the given constraints. Therefore, it gives the user the option to choose from the feasible solutions through specifying an aspect ratio or by selecting the optimum solution from the Pareto front of the generated shape function. In contrast to most of the existing techniques, as the number of physical constraints increases the SMT solver processing time decreases. The proposed system yielded layouts with a competitive area and run time compared to other techniques.