請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/37725
標題: | 在電路上實現之布林函數解法器以及它在利用電路重新連線進行邏輯最佳化之應用 A Circuit-Based Boolean Solver and Its Application to Rewiring-Based Logic Optimization |
作者: | Chi-An Wu 吳濟安 |
指導教授: | 黃鐘揚(Chung-Yang Huang) |
關鍵字: | 滿足性問題,縮減函式的邏輯閘且反向圖形,虛擬布林,多餘連線之移除及加入,邏輯合成,最佳化與驗證, Boolean Satisfiability (SAT),functionally reduced AND-INV graph (FRAIG),pseudo Boolean (PB),redundancy addition and removal (RAR),logic synthesis,optimization and verification, |
出版年 : | 2008 |
學位: | 碩士 |
摘要: | 在本論文中,我們提出了一個以滿足性解法為基礎的邏輯最佳化平台,它包含了在電路上建全的布林滿足性解法器、強力的多餘連線之移除及加入工具、和虛擬布林最佳器,它可以被用來做超大規模積體電路的驗證和邏輯最佳化。這個滿足性解法器是被實行在縮減函式的邏輯閘「且-反向」圖形之結構上,因此它在半標準型態的電路上有比較強的蘊涵能力。此外,我們提昇了這個圖形表示法讓它記錄更多邏輯蘊涵和允許多輸入的閘,且不同於其他人的滿足性解法器是透過合取範式為基礎,我們直接在此電路圖形上實踐滿足性解法器以獲得完全的結構資訊。而且我們綜合了滿足性解法中的變數決定法,和多餘連線之移除及加入演算法,使其更有的彈性和效率。最後,我們將滿足性解法器延伸到虛擬布林最佳化引擎,並創造了多重的多餘連線之移除及加入技術。我們應用此技術到電路最佳化問題上,實驗數據顯示出我們的架構相對於原本的方法有重大的改善。 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. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/37725 |
全文授權: | 有償授權 |
顯示於系所單位: | 電機工程學系 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-97-1.pdf 目前未授權公開取用 | 421.16 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。