完整後設資料紀錄
DC 欄位語言
dc.contributor.author張佳伶en_US
dc.contributor.authorChang, Chia-Lingen_US
dc.contributor.author溫宏斌en_US
dc.contributor.authorWen, Hung-Pinen_US
dc.date.accessioned2014-12-12T01:15:04Z-
dc.date.available2014-12-12T01:15:04Z-
dc.date.issued2008en_US
dc.identifier.urihttp://140.113.39.130/cdrfb3/record/nctu/#GT009513584en_US
dc.identifier.urihttp://hdl.handle.net/11536/38429-
dc.description.abstract為了確認二個不同版本的時序電路是否有相同的功能,最常見的方法 是將電路展開到限定的數量進行驗證,此方法稱為有界時序等價驗證 。雖然布林可滿足性解答器的大幅進展已經使得組合電路的等價驗證 上,可以應用至大型的電路,但其解答器在解決時序電路或有界時序 電路的問題時仍然非常沒有效率。因此,本論文提出一個利用三階段 的開發方法尋找電路的限制點,如此可以加速布林可滿足性解答器在有界時序電路上的應用。這些限制點主要由時序電路上的正反器組合而成。首先,我們會利用資料探勘的方法得到每個正反器的近似函數,再由這些函數的組合找出不會同時發生的狀態組合,此則稱為限制點。被找出的限制點會再被確認是否與模擬的資料相符。最後,有界時序電路會針對這些限制點逐一驗證,通過驗證的限制點,才是有界時序電路上真實的限制點。完成三階段尋找限制點的流程之後,所有的限制點會再被加回有界時序電路中,如此可以加速布林可滿足性解答器的解答過程。實驗結果證明,對於ISCAS89電路的有界時序驗證可以達到平均40倍的加速。zh_TW
dc.description.abstractOne 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.en_US
dc.language.isoen_USen_US
dc.subject功能性驗證zh_TW
dc.subject資料探勘zh_TW
dc.subject布林可滿足性問題zh_TW
dc.subjectfunctional verificationen_US
dc.subjectdata miningen_US
dc.subjectBoolean satisfiability problemen_US
dc.title應用資料探勘的有界時序電路等價驗證之加速方法設計zh_TW
dc.titleSpeeding up Bounded Sequential Equivalence Checking with Data Miningen_US
dc.typeThesisen_US
dc.contributor.department電信工程研究所zh_TW
顯示於類別:畢業論文


文件中的檔案:

  1. 358403.pdf

若為 zip 檔案,請下載檔案解壓縮後,用瀏覽器開啟資料夾中的 index.html 瀏覽全文。