Overview Statistic: PDF-Downloads (blue) and Frontdoor-Views (gray)

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

Additional Services

Share in Twitter Search Google Scholar Statistics - number of accesses to the document
Metadaten
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
Accept ✔
Diese Webseite verwendet technisch erforderliche Session-Cookies. Durch die weitere Nutzung der Webseite stimmen Sie diesem zu. Unsere Datenschutzerklärung finden Sie hier.