Name
Title | ||
|---|---|---|
Maximal input reduction of sequential netlists via synergistic reparameterization and localization strategies |
Abstract | ||
|---|---|---|
Automatic formal verification techniques generally require exponential resources with respect to the number of primary inputs of a netlist. In this paper, we present several fully-automated techniques to enable maximal input reductions of sequential netlists. First, we present a novel min-cut based localization refinement scheme for yielding a safely overapproximated netlist with minimal input count. Second, we present a novel form of reparameterization: as a trace-equivalence preserving structural abstraction, which provably renders a netlist with input count at most a constant factor of register count. In contrast to prior research in reparameterization to offset input growth during symbolic simulation, we are the first to explore this technique as a structural transformation for sequential netlists, enabling its benefits to general verification flows. In particular, we detail the synergy between these input-reducing abstractions, and with other transformations such as retiming which – as with traditional localization approaches – risks substantially increasing input count as a byproduct of its register reductions. Experiments confirm that the complementary reduction strategy enabled by our techniques is necessary for iteratively reducing large problems while keeping both proof-fatal design size metrics – register count and input count – within reasonable limits, ultimately enabling an efficient automated solution. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11560548_18 | CHARME |
Keywords | Field | DocType |
maximal input reduction,input growth,minimal input count,synergistic reparameterization,register reduction,overapproximated netlist,sequential netlists,input count,automatic formal verification technique,primary input,register count,localization strategy | Reduction strategy,Discrete mathematics,Netlist,Symbolic simulation,Retiming,Computer science,Circuit design,Algorithm,Formal methods,Offset (computer science),Formal verification | Conference |
Volume | ISSN | ISBN |
3725 | 0302-9743 | 3-540-29105-9 |
Citations | PageRank | References |
16 | 0.78 | 22 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jason Baumgartner | 1 | 313 | 23.36 |
| Hari Mony | 2 | 186 | 13.30 |