DocumentCode
2048500
Title
Exploiting suspected redundancy without proving it
Author
Mony, Hari ; Baumgartner, Jason ; Paruthi, Viresh ; Kanzelman, Robert
Author_Institution
IBM Syst. Group, Austin, TX, USA
fYear
2005
fDate
13-17 June 2005
Firstpage
463
Lastpage
466
Abstract
We present several improvements to general-purpose sequential redundancy removal. (1) We propose using a robust variety of synergistic transformation and verification algorithms to process the individual proof obligations. This enables greater speed and scalability, and identifies a significantly greater degree of redundancy, than prior approaches. (2) We generalize upon traditional redundancy removal and utilized the speculatively-reduced model to enhance bounded search, without needing to complete any proofs.
Keywords
formal verification; logic design; redundancy; sequential circuits; bounded search; correctness-preserving transformations; redundancy exploitation; sequential equivalence checking; sequential redundancy removal; speculatively reduced model; synergistic transformation; verification algorithms; Merging; Permission; Reachability analysis; Robustness; Scalability;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference, 2005. Proceedings. 42nd
Print_ISBN
1-59593-058-2
Type
conf
DOI
10.1109/DAC.2005.193853
Filename
1510373
Link To Document