90-04 Explicit machine computation and programs (not the theory of computation or programming)
Refine
Year of publication
- 2007 (1) (remove)
Document Type
- ZIB-Report (1)
Language
- English (1)
Has Fulltext
- yes (1)
Is part of the Bibliography
- no (1)
Keywords
- EigenschaftsprĂĽfer (1)
- constraint integer programming (1)
- formal chip verification (1)
- formale Chip Verifikation (1)
- micro chip (1)
- property checking (1)
- scip (1)
Institute
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.