Paper Info
Title
Speculative reduction-based scalable redundancy identification
Abstract
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.
Year
DOI
Venue
2009
10.1109/DATE.2009.5090932
DATE
Keywords
Field
DocType
redundancy assumption,proof obligation,sequential redundancy identification,redundancy identification process,speculative reduction-based scalable redundancy,induction-based redundancy identification,equivalence checking framework,redundancy identification,sequential synthesis,various proof technique,speculative reduction,algorithm design and analysis,interpolation,logic gates,component,logic,merging,data mining,virtualization,cost accounting,sequential circuits,equivalence checking,scalability,redundancy
Formal equivalence checking,Virtualization,Sequential logic,Algorithm design,Computer science,Real-time computing,Redundancy (engineering),Dual modular redundancy,Speedup,Scalability
Conference
ISSN
ISBN
Citations 
1530-1591
978-1-4244-3781-8
13
PageRank 
References 
Authors
0.81
19
4
Name
Order
Citations
PageRank
Hari Mony118613.30
Jason Baumgartner231323.36
Alan Mishchenko398284.79
Robert K. Brayton46224883.32