Exploiting suspected redundancy without proving it

We present several improvements to general-purpose sequential redundancy removal. First, we propose using a robust variety of synergistic transformation and verification algorithms to process the individual proof obligations. Experiments confirm that this more general approach enables greater speed and scalability, and identifies a significantly greater degree of redundancy, than previous approaches. Second, we demonstrate how we may generalize upon traditional redundancy removal applications and utilize the speculatively-reduced model to enhance bounded search, without needing to complete any proofs.

• Type: Conference
• Year: 2005
• Where: DAC
• Authors: Hari Mony, Jason Baumgartner, Viresh Paruthi, Robert Kanzelman
• Keywords: DAC 2005, Design Automation, Enables Greater Speed, Sequential Redundancy Removal, Traditional Redundancy Removal