STABLE: A new QF-BV SMT solver for hard verification problems combining Boolean reasoning with computer algebra
STABLE: A new QF-BV SMT solver for hard verification problems combining Boolean reasoning with computer algebra
复制标题
STABLE：一种新的 QF-BV SMT 求解器，用于结合布尔推理与计算机代数的硬验证问题
DOI：
10.1109/date.2011.5763035
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
G. Greuel
中科院分区：
文献类型：
--
作者：
Evgeny Pavlenko;Markus Wedler;D. Stoffel;W. Kunz;A. Dreyer;Frank Seelisch;G. Greuel
本文为固定尺寸的位矢量（QF-BV）的公式提供了一个新的SMT求解器。稳定的核心是基于计算机代数的发动机，它提供了用于简化SMT实例的算术问题的算法。作为稳定的主要应用程序域，我们针对基于SMT的属性检查流，用于片上系统（SOC）设计。验证工业数据路径模块时，我们经常遇到在使用硬件说明语言的逻辑级别指定的自定义设计的算术组件。这会导致SMT问题，其中算术部分可能包括非算术约束。稳定包括一种新技术，用于为这些非砷限制提取算术比位信息。因此，我们的代数发动机可以解决与整个算术设计组件相关的子问题。与其他最先进的SMT求解器相比，在大量的SMT公式中，成功评估了Stable，这些SMT公式描述了包括乘法在内的工业数据路径设计的验证问题。与其他求解器相反，稳定的稳定器能够以最多64位的位宽度解决实例。
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.