TY - GEN A1 - Achterberg, Tobias A1 - Brinkmann, Raik A1 - Wedler, Markus T1 - Property Checking with Constraint Integer Programming N2 - 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. T3 - ZIB-Report - 07-37 KW - formale Chip Verifikation KW - constraint integer programming KW - scip KW - Eigenschaftsprüfer KW - formal chip verification KW - constraint integer programming KW - scip KW - property checking KW - micro chip Y1 - 2007 UR - https://opus4.kobv.de/opus4-zib/frontdoor/index/index/docId/1037 UR - https://nbn-resolving.org/urn:nbn:de:0297-zib-10376 SN - 1438-0064 ER -