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.

Download full text files

Export metadata

  • Export Bibtex

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Tobias Achterberg, 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

$Rev: 13581 $