Sciweavers

Share
DATE
2009
IEEE

Speculative reduction-based scalable redundancy identification

9 years 3 months ago
Speculative reduction-based scalable redundancy identification
The process of sequential redundancy identification is the cornerstone of sequential synthesis and equivalence checking frameworks. The scalability of the proof obligations inherent in redundancy identification hinges not only upon the ability to cross-assume those redundancies, but also upon the way in which these assumptions are leveraged. In this paper, we study the technique of speculative reduction for efficiently modeling redundancy assumptions. We provide theoretical and experimental evidence to demonstrate that speculative reduction is fundamental to the scalability of the redundancy identification process under various proof techniques. We also propose several techniques to speed up induction-based redundancy identification. Experiments demonstrate the effectiveness of our techniques in enabling substantially faster redundancy identification, up to six orders of magnitude on large designs.
Hari Mony, Jason Baumgartner, Alan Mishchenko, Rob
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2009
Where DATE
Authors Hari Mony, Jason Baumgartner, Alan Mishchenko, Robert K. Brayton
Comments (0)
books