- 學位論文
運用可滿足性求解於安全賽局及低功率狀態滯留電路之可擴充性合成
Scalable Synthesis of Safety Games and Low-Power Retention Using Satisfiability Solving
摘要
在電子設計自動化領域中，許多困難的最佳化以及決定性問題可以公式化成可滿足性問題(satisfiability problem)並利用可滿足性求解器(SAT solver)來獲得答案。在過去數十年間，許多研究的貢獻讓可滿足性求解器變得有效率且效果優異。如正規驗證以及邏輯合成等等許多的應用因為採用了可滿足性求解器作為其求解核心因此在效能上顯著地受益於可滿足性求解器的進步。在這篇論文中，我們將前瞻的可滿足性問題求解技術運用到兩個問題上，分別是反應性系統的合成(synthesis of reactive systems)以及低功率電路設計中狀態滯留暫存器(retention register)的數量最佳化，在第一個問題中，我們受到當今最先進的模型檢驗(model checking)演算法 - 性質導向可達度(property-directed reachability, PDR, 又稱IC3)的啟發，採用了應用在量化布林函式(quantified Boolean formula, QBF)求解的交互式可滿足性求解(interactive SAT solving)技術並提出了一個基於可滿足性求解的合成演算法。在第二個問題中，我們使用了漸進式可滿足性求解(incremental SAT solving)、高階的符號模擬（symbolic simulation）以及不滿足核心(UNSAT core)的分析等技術以大幅降低問題的複雜度。實驗結果證實，在第一個問題中我們提出的演算法勝過了現有的基於可滿足性求解以及基於量化布林函式求解的方法，而在第二個問題中，我們提出的演算法強度足以應付業界等級的電路設計。
並列摘要
In the domain of electronic design automation (EDA), various tough combinatorial optimization and decision can be formulated as the satisfiability (SAT) problem and tackled by advanced SAT solvers. For the past decades, extensive efforts have been devoted to make SAT solver efficient. Many applications, such as formal verification and logic synthesis, adopt SAT solvers as the core engine and benefit greatly from the improvement of SAT solvers. In this thesis, we apply advanced SAT solving techniques to two applications, synthesis of reactive systems from safety specifications and retention register minimization in low-power design. For the former, we are inspired by the state-of-the-art model checking algorithm emph{property-directed reachability} (PDR, a.k.a. IC3) and propose a SAT-based synthesis algorithm that extends the PDR by adopting the concept of interactive SAT solving for two-level quantified Boolean formulas (2QBF). For the latter, we exploit incremental SAT solving, high level symbolic simulation and unsatisfiable (UNSAT) core analysis to greatly reduce runtime overhead. Experimental results show that our proposed algorithm for the former problem outperform the existing SAT-based and QBF-based algorithms by some margin and the method for the latter problem is effectively applicable to industrial designs.