使用布林滿足性求解的邏輯與實體合成

Logic and Physical Syntheses via SAT Solving

張鶴騰(He-Teng Zhang)

指導教授 ： 江介宏 ； 藤田昌宏 ； Alan Mishchenko

國立臺灣大學/電機資訊學院/電子工程學研究所/博士(2022年)

https://doi.org/10.6342/NTU202210157

摘要

隨著先進製程進步以及對電子系統的需求，邏輯合成與實體設計的融合引起廣泛的注意。從邏輯合成的觀點來看，SAT求解器是一種易於擴展且通用的布林推理引擎，被廣泛應用在科學研究或者工業/商業領域。據近期文獻，由於SAT求解器的使用彈性與可延展性，其可能為IC設計流程帶來更好的效率與設計品質。

本研究探索了SAT相關主題的數個層面，包含電子設計自動化流程中的前段與後段設計，並最終為SAT求解器本身做出創新。對於前段設計，我們提升了SAT sweeping的可延展性，以利於更有效地應對大型晶片設計。對於後段設計，我們為排線繞線提出了基於圖與SAT的混合繞線框架並使用了新的編碼方式，這為SAT於後段設計的使用提供新思考方式與彈性。接著，我們探索了實體感知的邏輯合成於ECO的應用，展示了將EDA流程中前、後段設計聯繫起來的方式。除了上述基於SAT的應用之外，根據我們近期在SAT求解的新發現，提出基於電路/CNF的混合SAT求解器，並在大型電路的解析過程中展現了顯著的效能提升。

關鍵字

布林可滿足性 ； 邏輯合成與驗證 ； 排線繞線 ； 工程變更 ； 布林求解器 ； 基於電路的混合布林求解器 ； 基於布林可滿足性的等價化簡 ； 邏輯辯證 ； 模擬

並列摘要

With the advancing technology node and the demand for competitive electronic systems, the fusion of logic synthesis and physical design draws wide attention. From a logic synthesis view, SAT solver is a scalable and generic Boolean reasoning engine widely used in scientific research or industrial/commercial applications. Recent works indicate SAT solvers provide more flexibility in various design scenarios, scale up algorithms, and could bring essential improvement to the quality or efficiency of the IC design process.

In this work, we explore SAT-related topics covering several aspects, from frontend to backend design in EDA flow, and eventually bring novel ideas to SAT solve itself. In the frontend design phase, SAT sweeping is scaled up to match the modern design size. In the backend design phase, a graph/SAT-based hybrid framework for bus routing using new encoding is proposed, which brings a different way of treating physical design problems with SAT. Furthermore, a physical-aware logic synthesis problem related to ECO is explored, demonstrating a way of correlating the frontend and backend design in EDA flow. In addition to the above SAT-based applications in EDA, we propose a new circuit/CNF-based hybrid SAT solver using our recent findings in theoretical SAT solving, which delivers dramatic speedup in optimizing large-scale designs.

並列關鍵字

Boolean Satisfiability (SAT) ； Logic synthesis and verification ； Bus routing ； Engineering change order ； SAT Solver ； Circuit-based hybrid SAT Solver ； SAT sweeping ； Logic justification ； Simulation

參考文獻

[1] K. A. Dynamic transition relation simplification for bounded property checking. In Proceedings of International Conference on Computer-Aided Design (ICCAD), 2004.

[2] A. Abdollahi and M. Pedram. Symmetry detection and boolean matching utilizing a signature-based canonical form of boolean functions. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 27(6):1128– 1137, 2008.

[3] L. Amarú, F. Marranghello, E. Testa, C. Casares, V. Possani, J. Luo, P. Vuillod, A. Mishchenko, and G. D. Micheli. SAT-sweeping enhanced for logic synthesis. In Proceedings of Design Automation Conference (DAC), 2020.

[4] G. Audemard and L. Simon. SAT solver Glucose 3.0 (2013). http://www.labri.fr/ perso/lsimon/glucose/.

[5] V. Balabanov and J.-H. R. Jiang. Unified QBF certification and its applications. Formal Methods in System Design, 41(1):45–65, 2012.