標題: Mining Unreachable Cross-timeframe State-pairs for Bounded Sequential Equivalence Checking
作者: Chang, Lynn C. -L
Wen, Charles H. -P.
電信工程研究所
Institute of Communications Engineering
公開日期: 2009
摘要: 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.
URI: http://hdl.handle.net/11536/16685
http://dx.doi.org/10.1109/MTV.2008.23
ISBN: 978-0-7695-3581-4
ISSN: 1550-4093
DOI: 10.1109/MTV.2008.23
期刊: MTV 2008: NINTH INTERNATIONAL WORKSHOP ON MICROPROCESSOR TEST AND VERIFICATION, PROCEEDINGS
起始頁: 33
結束頁: 38
顯示於類別:會議論文


文件中的檔案:

  1. 000271214900006.pdf

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