European Design and Automation Association
In this paper, the authors present 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 they target an SMT-based property checking flow for System-on-Chip (SoC) designs. When verifying industrial data path modules they frequently encounter custom-designed arithmetic components specified at the logic level of the hardware description language being used.