Name
Abstract | ||
|---|---|---|
Industrial verification and synthesis tools routinely identify and eliminate redundancies from logic designs. In the former case, redundancy removal yields critical speedups to the overall verification process. In the latter case, redundancy removal constitutes a primary mechanism to optimize the final fabricated circuit. Redundancy identification frameworks often utilize a greatest-fixedpoint iteration, initially postulating a set of candidate redundancies to be conjunctively proved then refining candidates based upon failed proof attempts. Such procedures generally do not yield any soundly-proved redundancies until a fixedpoint is achieved. In this paper, we overcome this drawback by augmenting the fixedpoint procedure with a set of efficient techniques to track dependencies between candidate redundancies. This approach enables the identification of an optimal subset of valid redundancies before the fixedpoint is reached, and may also be used to reduce the number of computations within the fixedpoint procedure. We apply our techniques to enhance k-induction as well as a more general transformation-based verification flow. For induction, we demonstrate up to 75% reduction in runtime and 97% reduction in the number of inductive proofs. For the more general flow, we demonstrate up to 90% reduction in runtime and 80% reduction in the total number of proof obligations. |
Year | Venue | Keywords |
|---|---|---|
2011 | FMCAD | optimal redundancy removal,industrial verification,former case,general transformation-based verification flow,total number,fixedpoint procedure,failed proof attempt,overall verification process,redundancy identification,candidate redundancy,general flow,fixedpoint computation,algorithm design and analysis,theorem proving,formal verification,redundancy,merging,algorithm design,logic gate,logic design,logic gates,iterative methods |
Field | DocType | Citations |
Logic synthesis,Algorithm design,Computer science,Iterative method,Automated theorem proving,Algorithm,Theoretical computer science,Mathematical proof,Redundancy (engineering),Computation,Formal verification | Conference | 0 |
PageRank | References | Authors |
0.34 | 11 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Case | 1 | 44 | 6.66 |
| Jason Baumgartner | 2 | 313 | 23.36 |
| Hari Mony | 3 | 186 | 13.30 |
| Robert Kanzelman | 4 | 107 | 6.16 |