標題: 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
Appears in Collections:Conferences Paper


Files in This Item:

  1. 000271214900006.pdf

If it is a zip file, please download the file and unzip it, then open index.html in a browser to view the full text content.