Satisfiability-Based Methods for Digital Circuit Design, Debug, and Optimization
Satisfiability-Based Methods for Digital Circuit Design, Debug, and Optimization
复制标题
基于可满足性的数字电路设计、调试和优化方法
DOI：
10.5075/epfl-thesis-8850
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Andrew Becker
中科院分区：
文献类型：
--
作者：
Andrew Becker
设计好数字电路是出了名的困难。这种困难部分源于电路设计中固有的许多自由度，通常还需要满足各种约束条件。在本文中，我们展示了如何自动使用可满足性问题的公式来完成设计，或找到满足某些约束的特定设计架构；如何使用这些工具来创建、调试和优化设计；并引入一种特别适合于满意度辅助设计、调试和优化的领域特定语言。在第一个应用中，我们展示了被称为“洞”的显式不确定性是如何自然使用的，并且有助于创建对设计电路有用的形式可满足性问题。我们进一步开发了一种scala托管的领域特定语言（DSL），它具有适当的语法糖，使带漏洞的设计变得简单有效。然后，我们将展示如何利用相同的可满足性公式，自动检测给定的错误设计，用可能正确的替代方案替换可疑的语法片段。然后，满意度求解器确定是否存在任何可能的可选片段集来修复错误。我们还证明了这种方法是合理可伸缩的，部分原因是在可满足性问题的表述中不太需要完全精确的规范。然后，我们超越了单纯的填空，并展示了如何将设计精细化与可满足性求解器紧密集成，从而实现全新的方法。为了指出这一点，我们使用这种紧密集成来创建第一个已知的方法来优化门级信息流跟踪（GLIFT）模型电路，并在其精度上做出原则性的权衡。最后，综合之前的所有工作，我们提出了一个更强大的DSL，专门用于解决第一个“填补漏洞”语言的缺点。这种语言，我们称之为Nasadiya，为电路设计和优化提供了更通用的可满足性集成，并提供了内置的建模功能，用于优化关键路径延迟和电路面积等额外功能属性。我们通过为一种流行的并行前缀加法器实现自动功率优化器来演示这些特性的实用性。
Designing digital circuits well is notoriously difficult. This difficulty stems in part from the very many degrees of freedom inherent in circuit design, typically coupled with the need to satisfy various constraints. In this thesis, we demonstrate how formulations of satisfiability problems can be used automatically to complete a design, or to find a specific design architecture that satisfies certain constraints; how these can be used to create, debug, and optimize designs; and introduce a domain-specific language particularly well-suited for satisfiability-assisted design, debug, and optimization. In the first application, we show how explicit uncertainties called “holes” can both be natural to use and conducive to the creation of formal satisfiability problems useful for designing circuits. We further develop a Scala-hosted Domain Specific Language (DSL) with appropriate syntactic sugar to make design with holes easy and effective. We then show how, utilizing the same kind of satisfiability formulation, we can automatically instrument a given buggy design to replace suspicious syntax fragments with potentiallycorrect alternatives. The satisfiability solver then determines if there is any possible set of alternative fragments which fix the bug. We also demonstrate that this approach is reasonably scalable, in part because there is less need for a fully-precise specification in the formulation of the satisfiability problem. We then advance beyond mere hole-filling and show how a tight integration of design elaboration with satisfiability solvers allows totally new approaches. To point, we use this tight integration to create the first known methods to optimize Gate-Level Information Flow Tracking (GLIFT) model circuits and to make principled trade-offs in their precision. Finally, integrating all the previous work, we propose a more powerful DSL specifically designed to address the shortcomings of the first “hole-filling” language. This language, which we call Nasadiya, affords more general integrations of satisfiability into circuit design and optimization, and provides built-in modeling functionality useful for optimizing extra-functional properties like critical path delay and circuit area. We demonstrate the utility of these features by implementing an automatic power optimizer for a popular type of parallel prefix adders.
DOI：
10.1016/j.istr.2009.06.001
发表时间：
2009-05
期刊：
Inf. Secur. Tech. Rep.
影响因子：
--
作者：
K. Markantonakis;Michael Tunstall;G. Hancke;Ioannis G. Askoxylakis;K. Mayes
通讯作者：
K. Markantonakis;Michael Tunstall;G. Hancke;Ioannis G. Askoxylakis;K. Mayes