Mining unreachable cross-timeframe state-pairs for bounded sequential equivalence checking

Lynn C.L. Chang, Charles H.P. Wen

研究成果: Conference contribution同行評審

摘要

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.

原文English
主出版物標題9th International Workshop on Microprocessor Test and Verification
主出版物子標題Common Challenges and Solutions, MTV 2008
發行者Institute of Electrical and Electronics Engineers Inc.
頁面33-38
頁數6
ISBN(列印)9780769535814
DOIs
出版狀態Published - 1 一月 2008
事件2009 9th International Workshop on Microprocessor Test and Verification: Common Challenges and Solutions, MTV 2008 - Austin, TX, United States
持續時間: 8 十二月 200810 十二月 2008

出版系列

名字Proceedings - International Workshop on Microprocessor Test and Verification
ISSN(列印)1550-4093

Conference

Conference2009 9th International Workshop on Microprocessor Test and Verification: Common Challenges and Solutions, MTV 2008
國家United States
城市Austin, TX
期間8/12/0810/12/08

指紋 深入研究「Mining unreachable cross-timeframe state-pairs for bounded sequential equivalence checking」主題。共同形成了獨特的指紋。

引用此