Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

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

: Pavlenko, E.; Wedler, M.; Stoffel, D.; Kunz, W.; Dreyer, A.; Seelisch, F.; Greuel, G.-M.

Institute of Electrical and Electronics Engineers -IEEE-; European Design Automation Association -EDAA-:
Design, Automation & Test in Europe Conference & Exhibition, DATE 2011. Proceedings. Vol.1 : Grenoble, France, 14 - 18 March 2011
Piscataway/NJ: IEEE, 2011
ISBN: 978-1-61284-208-0
ISBN: 978-3-9810801-7-9
Design, Automation and Test in Europe Conference (DATE) <14, 2011, Grenoble>
Conference Paper
Fraunhofer ITWM ()

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.