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

Abstract

隨著先進製程進步以及對電子系統的需求，邏輯合成與實體設計的融合引起廣泛的注意。從邏輯合成的觀點來看，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.