Name
Abstract | ||
|---|---|---|
This work presents a technology-independent synthesis optimization that is effective in reducing the total number of state elements of a design. It works by identifying and eliminating dependent state elements which may be expressed as functions of other registers. For scalability, we rely exclusively on SAT-based analysis in this process. To enable optimal identification of all dependent state elements, we integrate an inductive invariant generation framework. We introduce numerous techniques to heuristically enhance the reduction potential of our method, and experiments confirm that our approach is scalable and is able to reduce state element count by 12% on average in large industrial designs, even after other aggressive optimizations such as minregister retiming have been applied. The method is effective in simplifying later verification efforts. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/FMCAD.2008.ECP.6 | FMCAD |
Keywords | Field | DocType |
state element,state element count,dependent state element,later verification effort,minregister retiming,large industrial design,inductive invariant generation framework,invariant-strengthened elimination,numerous technique,aggressive optimizations,sat-based analysis,logic synthesis,registers,scalability,formal verification,optimization,data structures,industrial design,boolean functions,algorithm design and analysis,cost accounting,computability | Boolean function,Retiming,Data structure,Algorithm design,Computer science,Algorithm,Computability,Theoretical computer science,Invariant (mathematics),Formal verification,Scalability | Conference |
ISBN | Citations | PageRank |
978-1-4244-2736-9 | 4 | 0.43 |
References | Authors | |
13 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael L. Case | 1 | 52 | 4.02 |
| Alan Mishchenko | 2 | 982 | 84.79 |
| Robert K. Brayton | 3 | 6224 | 883.32 |
| Jason Baumgartner | 4 | 313 | 23.36 |
| Hari Mony | 5 | 186 | 13.30 |