在電路上實現之布林函數解法器以及它在利用電路重新連線進行邏輯最佳化之應用

Abstract

在本論文中，我們提出了一個以滿足性解法為基礎的邏輯最佳化平台，它包含了在電路上建全的布林滿足性解法器、強力的多餘連線之移除及加入工具、和虛擬布林最佳器，它可以被用來做超大規模積體電路的驗證和邏輯最佳化。這個滿足性解法器是被實行在縮減函式的邏輯閘「且-反向」圖形之結構上，因此它在半標準型態的電路上有比較強的蘊涵能力。此外，我們提昇了這個圖形表示法讓它記錄更多邏輯蘊涵和允許多輸入的閘，且不同於其他人的滿足性解法器是透過合取範式為基礎，我們直接在此電路圖形上實踐滿足性解法器以獲得完全的結構資訊。而且我們綜合了滿足性解法中的變數決定法，和多餘連線之移除及加入演算法，使其更有的彈性和效率。最後，我們將滿足性解法器延伸到虛擬布林最佳化引擎，並創造了多重的多餘連線之移除及加入技術。我們應用此技術到電路最佳化問題上，實驗數據顯示出我們的架構相對於原本的方法有重大的改善。

In this thesis, we proposed a SAT-based logic optimization framework which contains a robust Boolean satisfiability (SAT) solver, a powerful redundancy-addition-and- removal (RAR) engine, and a Pseudo-Boolean optimizer on the circuit netlist. It can be used for the verification and logic optimization of the VLSI circuits. The SAT solver is implemented on the FRAIG (Functionally Reduced And-Inverter Graph) structure so that it has stronger implicability on a semi-canonical circuit netlist. We further revised the FRAIG by recording more logic implications and allowing multi-input gates. Different from other FRAIG packages where the SAT engine is based on a separated Conjunctive-Normal-Form (CNF) based solver, we implemented the SAT algorithms directly on FRAIG so that the structural information can be fully utilized. Moreover, we incorporated the SAT decision making and RAR techniques so that the RAR-based logic optimization can be more flexible and efficient. Lastly, we extended our SAT solver to a Pseudo Boolean (PB) optimizer and proposed a multiple RAR technique. We applied these techniques for circuit optimization and the experimental results show that our framework can achieve significant improvement over the traditional approaches.