利用可調整內插法計算邏輯無關項

Abstract

近年來在邏輯合成與驗證的領域中，內插法的應用與日俱增，相關範疇包括函數相依、二元分解、亞氏分解等。本研究係利用內插法針對多層次電路之節點計算邏輯無關項。 傳統上，內插可藉由可滿足性問題求解器產生之反證求得，並可利用改寫反證之結構對內插大小進行調整。但我們在研究過程發現，大部分狀況中，調整可滿足性問題求解器產生反證後所求得之內插並無太大的改變，內插法的效能因而受限。 本論文中，我們提出利用可滿足性問題求解之演算法來計算邏輯無關項，並發展出一套針對可滿足性問題求解器改變內插大小的技巧，包括調整初始變數優先序及改變布林初始值，同時利用電路結構簡化問題模型以加快求解速度。實驗結果顯示，該改變內插大小的方法讓求解邏輯無關項之演算法在可接受的時間內，較未使用該方法時求出更多的邏輯無關項。

In recent years, there have been a variety of applications of interpolation in logic synthesis and verification, such as functional dependency, bi-decomposition, and Ashenhurst decomposition. The goal of this research is to compute don’t-cares for a given node in a multi-level network by using interpolation. Traditionally, an interpolant can be derived from a refutation proof given by a SAT solver, and its onset can be adjusted via rewriting the structure of the refutation proof. However, in most cases, the interpolant derived by the refutation proof generated by a SAT solver can not be adjusted too much. As a result, the application of interpolation is limited. In this thesis, we propose SAT-based don’t-care computation algorithms via interpolation. In addition, a set of techniques has been developed for a SAT solver to adjust the solution space of the interpolant. The methods include setting the initial variable activities and altering the Boolean initial values. The circuit structure has also been utilized to simplify the problem to accelerate SAT solving. Experiments show that the algorithms can get more don’t-cares while applying the interpolation sizing method to the algorithms.