STABLE: A new QF-BV SMT solver for hard verification problems combining Boolean reasoning with computer algebra

• Main Authors: Pavlenko, E, Wedler, M, Stoffel, D, Kunz, W, Dreyer, A, Seelisch, F, Greuel, G
• Format: Conference Proceeding
• Language: English
• Subjects: Adders; Algebra; Engines; Mathematical model; Polynomials; System-on-a-chip
• ISSN: 1530-1591; 1558-1101
• DOI: 10.1109/DATE.2011.5763035

This paper presents a new SMT solver, STABLE, for formulas of the quantifier-free logic over fixed-sized bit vectors (QF-BV). The heart of STABLE is a computer-algebra-based engine which provides algorithms for simplifying arithmetic problems of an SMT instance prior to bit-blasting. As the primary application domain for STABLE we target an SMT-based property checking flow for System-on-Chip (SoC) designs. When verifying industrial data path modules we frequently encounter custom-designed arithmetic components specified at the logic level of the hardware description language being used. This results in SMT problems where arithmetic parts may include non-arithmetic constraints. STABLE includes a new technique for extracting arithmetic bit-level information for these non-arithmetic constraints. Thus, our algebraic engine can solve subproblems related to the entire arithmetic design component. STABLE was successfully evaluated in comparison with other state-of-the-art SMT solvers on a large collection of SMT formulas describing verification problems of industrial data path designs that include multiplication. In contrast to the other solvers STABLE was able to solve instances with bit-widths of up to 64 bits.