Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. Solving hard instances in QFBV combining Boolean reasoning with computer algebra
 Becker, B.: Algorithms and Applications for Next Generation SAT Solvers : Dagstuhl Seminar 09461, 08.11.  13.11.2009 Wadern: Schloss Dagstuhl, LeibnizZentrum für Informatik, 2010 (Dagstuhl Seminar Proceedings 09461) ISSN: 18624405 20 pp. 
 Dagstuhl Seminar "Algorithms and Applications for Next Generation SAT Solvers" <2009, Schloß Dagstuhl> 

 English 
 Conference Paper, Electronic Publication 
 Fraunhofer ITWM () 
Abstract
This paper describes our new satisfyability (SAT) modulo theory (SMT) solver STABLE for the quantifierfree logic over fixed size bit vectors. Our main application domain is formal verification of systemonchip (SoC) modules designed for complex computational tasks, for example, in signal processing applications. Ensuring proper functional behavior for such modules, including arithmetic correctness of the data paths, is considered a very difficult problem. We show how methods from computer algebra can be integrated into an SMT solver such that instances can be handled where the arithmetic problem parts are specified mixing various levels of abstraction from the plain gate level for small highly optimized components up to the pure word level used in highlevel specifications. If the arithmetic problem parts include multiplications such mixed problem descriptions quickly drive current SMT solvers towards their capacity limits. High performance data paths are often designed at a level of abstraction that we call the arithmetic bit level (ABL). We show how ABL information, if available in an SMT instance, can be used to transform the decision problem into an equivalent set of variety subset problems. These problems can be solved efficiently with techniques from computer algebra based on Gröbner basis theory over finite rings Z/2n . Sometimes, instances contain problem parts at a level below the ABL using gatelevel operations. These problem parts, e.g., originate from customdesigned arithmetic components that are highly optimized using the gatelevel constructs of a hardware description language (HDL). For such cases we integrate a local ABL extraction technique based on local ReedMuller forms.