Back to Search
Start Over
Input Elimination Transformations for Scalable Verification and Trace Reconstruction
- Source :
- FMCAD
- Publication Year :
- 2019
- Publisher :
- IEEE, 2019.
-
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%.
- Subjects :
- Speedup
Computer science
Computation
Scalability
0202 electrical engineering, electronic engineering, information engineering
Netlist
Leverage (statistics)
020201 artificial intelligence & image processing
02 engineering and technology
Merge (version control)
Algorithm
020202 computer hardware & architecture
Subjects
Details
- Database :
- OpenAIRE
- Journal :
- 2019 Formal Methods in Computer Aided Design (FMCAD)
- Accession number :
- edsair.doi...........9002210bef82a86bebf9d589b70e5375