Property Checking with Constraint Integer Programming
Please always quote using this URN: urn:nbn:de:0297-zib-10376
- We address the property checking problem for SoC design verification at the register transfer level (RTL) by integrating techniques from integer programming, constraint programming, and SAT solving. Specialized domain propagation and preprocessing algorithms for individual RTL operations extend a general constraint integer programming framework. Conflict clauses are learned by analyzing infeasible LPs and deductions, and by employing reverse propagation. Experimental results show that our approach outperforms SAT techniques for proving the validity of properties on circuits containing arithmetics.
Author: | Tobias AchterbergORCiD, Raik Brinkmann, Markus Wedler |
---|---|
Document Type: | ZIB-Report |
Tag: | Eigenschaftsprüfer; constraint integer programming; formale Chip Verifikation; scip constraint integer programming; formal chip verification; micro chip; property checking; scip |
MSC-Classification: | 90-XX OPERATIONS RESEARCH, MATHEMATICAL PROGRAMMING / 90-04 Explicit machine computation and programs (not the theory of computation or programming) |
90-XX OPERATIONS RESEARCH, MATHEMATICAL PROGRAMMING / 90-08 Computational methods | |
90-XX OPERATIONS RESEARCH, MATHEMATICAL PROGRAMMING / 90Cxx Mathematical programming [See also 49Mxx, 65Kxx] / 90C11 Mixed integer programming | |
90-XX OPERATIONS RESEARCH, MATHEMATICAL PROGRAMMING / 90Cxx Mathematical programming [See also 49Mxx, 65Kxx] / 90C57 Polyhedral combinatorics, branch-and-bound, branch-and-cut | |
Date of first Publication: | 2007/11/21 |
Series (Serial Number): | ZIB-Report (07-37) |
ISSN: | 1438-0064 |
ZIB-Reportnumber: | 07-37 |