Title :
Exploiting suspected redundancy without proving it
Author :
Mony, Hari ; Baumgartner, Jason ; Paruthi, Viresh ; Kanzelman, Robert
Author_Institution :
IBM Syst. Group, Austin, TX, USA
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;
Conference_Titel :
Design Automation Conference, 2005. Proceedings. 42nd
Print_ISBN :
1-59593-058-2
DOI :
10.1109/DAC.2005.193853
