| Title | Input Elimination Transformations for Scalable Verification and Trace Reconstruction |
| Publication Type | Conference Paper |
| Year of Publication | 2019 |
| Authors | Gajavelly, Raj Kumar, Baumgartner, Jason, Ivrii, Alexander, Kanzelman, Robert L., Ghosh, Shiladitya |
| Conference Name | 2019 Formal Methods in Computer Aided Design (FMCAD) |
| Keywords | 2QBF variant, Complexity theory, compositionality, computational complexity, connectivity verification, Cost accounting, fast- lossy preprocess, formal verification, input elimination transformations, input reparameterization, Logic gates, merging, model checking, netlist transformations, Predictive Metrics, pubcrawl, Registers, Resiliency, Scalability, scalable verification, trace reconstruction, verification complexity, verification scalability |
| Abstract | We present two novel sound and complete netlist transformations, which substantially improve verification scalability while enabling very efficient trace reconstruction. First, we present a 2QBF variant of input reparameterization, capable of eliminating inputs without introducing new logic and without complete range computation. While weaker in reduction potential, it yields up to 4 orders of magnitude speedup to trace reconstruction when used as a fast-and-lossy preprocess to traditional reparameterization. Second, we present a novel scalable approach to leverage sequential unateness to merge selective inputs, in cases greatly reducing netlist size and verification complexity. Extensive benchmarking demonstrates the utility of these techniques. Connectivity verification particularly benefits from these reductions, up to 99.8%. |
| DOI | 10.23919/FMCAD.2019.8894294 |
| Citation Key | gajavelly_input_2019 |
Input Elimination Transformations for Scalable Verification and Trace Reconstruction