應用資料探勘的有界時序電路等價驗證之加速方法設計

Abstract

為了確認二個不同版本的時序電路是否有相同的功能，最常見的方法 是將電路展開到限定的數量進行驗證，此方法稱為有界時序等價驗證 。雖然布林可滿足性解答器的大幅進展已經使得組合電路的等價驗證 上，可以應用至大型的電路，但其解答器在解決時序電路或有界時序 電路的問題時仍然非常沒有效率。因此，本論文提出一個利用三階段 的開發方法尋找電路的限制點，如此可以加速布林可滿足性解答器在有界時序電路上的應用。這些限制點主要由時序電路上的正反器組合而成。首先，我們會利用資料探勘的方法得到每個正反器的近似函數，再由這些函數的組合找出不會同時發生的狀態組合，此則稱為限制點。被找出的限制點會再被確認是否與模擬的資料相符。最後，有界時序電路會針對這些限制點逐一驗證，通過驗證的限制點，才是有界時序電路上真實的限制點。完成三階段尋找限制點的流程之後，所有的限制點會再被加回有界時序電路中，如此可以加速布林可滿足性解答器的解答過程。實驗結果證明，對於ISCAS89電路的有界時序驗證可以達到平均40倍的加速。

One common practice of checking equivalence for two sequential circuits often limits the timeframe expansion to a fixed number, and is known as bounded sequential equivalence checking (BSEC). Although the recent advances of Boolean satisfiability (SAT) solvers make combinational equivalence checking scalable for large designs, solving BSEC problems by SAT remains computationally inefficient. Therefore, this paper proposes a 3-stage method to exploit constraints to facilitate SAT solving for BSEC. The candidate set are first accumulated by checking each composition of functions derived by a data-mining algorithm for every two cross-timeframe flip-flop states. Each candidate can be further removed if it matches simulation data in history and its validity is finally confirmed through gate-level netlist. The verified set is feedbacked as constraints in SAT solving for the original BSEC problem. Experimental results show a 40X speedup in average on ISCAS 89 circuits.