DocumentCode :
3041993
Title :
Sequential equivalence checking of hard instances with targeted inductive invariants and efficient filtering strategies
Author :
Huy Nguyen ; Hsiao, Michael S.
Author_Institution :
Bradley Dept. of Electr. & Comput. Eng., Virginia Tech, Blacksburg, VA, USA
fYear :
2012
fDate :
9-10 Nov. 2012
Firstpage :
1
Lastpage :
8
Abstract :
We propose two approaches to significantly boost the power of sequential equivalence checking: (1) In contrast with invariants involving only two or three signals, we introduce a novel multisignal invariant generation technique that is scalable to large circuits; (2) We utilize static and dynamic filters to reduce the number of potential inductive invariants that need to be proved to further reduce the computational cost. Experimental results show that the proposed method can handle hard SEC instances with little or no internal equivalences that conventional methods fail; in addition, one to three orders of magnitude speedup have been achieved for many instances.
Keywords :
filters; sequential circuits; dynamic filters; hard SEC instances; large circuits; magnitude speedup; multisignal invariant generation; power boost; sequential equivalence checking; static filters; targeted inductive invariants; Cognition; Computational efficiency; Databases; Encoding; Integrated circuit modeling; Logic gates; Sequential circuits;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
High Level Design Validation and Test Workshop (HLDVT), 2012 IEEE International
Conference_Location :
Huntington Beach, CA
ISSN :
1552-6674
Print_ISBN :
978-1-4673-2897-5
Type :
conf
DOI :
10.1109/HLDVT.2012.6418236
Filename :
6418236
Link To Document :
بازگشت