Please use this identifier to cite or link to this item:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/42381
Title: | 運用內插法及求解可滿足性之大型布林函數二元分解法 Bi-Decomposing Large Boolean Functions via Interpolation and Satisfiability Solving |
Authors: | Ruei-Rung Lee 李瑞榮 |
Advisor: | 江介宏(Jie-Hong Jiang) |
Keyword: | 二元分解法,變數分隔,克雷格內插法, bi-decomposition,variable partition,Craig interpolation., |
Publication Year : | 2009 |
Degree: | 碩士 |
Abstract: | 在邏輯合成裡,布林函式的二元分解是一項非常基本的動作,大致上來說,二元分解是一種特殊的函式分解,他將函式分解成二個較小的子函式,而這兩個子函式經過一個具有兩個輸入的邏輯閘就相等於原本的函式。二元分解的品質好壞取決於變數的分隔,一個好的變數分隔使得二元分解後的兩個子函式變數交集少而且數量差不多。這種好的分解可以降低電路的複雜度,進而簡化實體設計。 之前的方法建立在二元決策圖上,當函式的變數增大時,常因記憶體容量不足而無法計算,此外,只能在變數分隔以後,才能判斷函式是否可二元分解,造成大量的運算。
基於上述的原因,我們提出運用求解可滿足性的方法來檢查函式是否可二元分解,如果可以被二元分解的,利用克雷格內插法求出子函式,最重要的是,我們將變數分隔整合進求解可滿足性的過程中,換句話說,在檢查是否可二元分解之前,不需先指定好變數分隔就可以進行檢查,如果是可二元分解的話,可滿足性求解器會產生一組可行的變數分隔,實驗結果顯示,可以將二元分解應用到大型函式上面。 另外,當多個函式分開進行二元分解時,會得到多個子函式,如果有些子函式跟其他的子函式相等或差一個反相器的話,這些子函式就可以被彼此取代。如此一來,我們可以將多個函式分解成較少的子函式,更進一步地降低電路面積。因此,我們考慮同時將多個函式進行二元分解,使得一些子函式可以被共用。在這篇論文當中,我們考慮多個函式的”或邏輯閘”二元分解。實驗顯示這項技巧可以用來降低電路面積。 Boolean function bi-decomposition is a fundamental operation in logic synthesis. Roughly speaking, bi-decomposition is a special kind of decomposition which decomposes a function into a two-input function composed with two other input functions. Precisely speaking, a function f(X) is bi-decomposable under a variable partition XA,XB,XC on X if it can be written as h(fA(XA,XC), fB(XB,XC)) for some functions h, fA, and fB. The quality of a bi-decomposition is mainly determined by its variable partition. A good variable partition makes the decomposition disjoint, i.e. XC = ∅, and balanced, i.e. |XA| ≈ |XB|. Such a good decomposition reduces communication and circuit complexity, and yields simple physical design solutions. Prior BDD-based methods may not be scalable to the decomposition due to the memory explosion problem. Also as decomposability is checked under a fixed variable partition, searching a feasible or good partition may run through costly enumeration that requires separate and independent decomposability checkings. We propose a solution to check whether a function is bi-decomposable using incremental SAT solving. Then, we derive subfunctions by Craig interpolation if decomposable. Most importantly, we integrate the variable partition into SAT solving. In other words, we do not need to specify the variable partition before checking bi-decomposability. If the given function is bi-decomposable, the SAT solver will generate a feasible and non-trivial variable partition. When n functions are bi-decomposed separately, we have 2n subfunctions. If some subfunctions are complementary or identical to each other, then these subfunctions can be replaced with each other. By doing so, we can bi-decompose n functions to fewer than 2n subfunctions and reduce circuit size further. Accordingly, it motivates us to bi-decompose multiple functions simultaneously such that some subfunctions can be shared. In this thesis, we consider both single-output and Noutput bi-decomposition. Therefore, we use the term ”bi-decomposition” to denote single-output bi-decomposition. Besides, we focus on N-output or-decomposition. Experimental results show that the capacity of bi-decomposition can be scaled up substantially to handle large designs. Also it shows that 2-output or-decomposition can be used to reduce circuit size. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/42381 |
Fulltext Rights: | 有償授權 |
Appears in Collections: | 電子工程學研究所 |
Files in This Item:
File | Size | Format | |
---|---|---|---|
ntu-98-1.pdf Restricted Access | 1.3 MB | Adobe PDF |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.