Matching Multiplications in Bit-Vector Formulas

TL;DR

This paper introduces a pre-processing heuristic for bit-vector formulas in hardware verification that improves SMT solver performance on multiplication-heavy formulas by identifying and asserting equivalences of decomposed multipliers.

Contribution

The paper presents a novel heuristic that detects decomposed multipliers in bit-vector formulas and encodes their equivalence to word-level multiplication, enhancing solver efficiency.

Findings

Heuristic enables faster solving of certain formulas.

Pre-processing reduces timeouts in SMT solving.

Improves reasoning about decomposed multipliers.

Abstract

Bit-vector formulas arising from hardware verification problems often contain word-level arithmetic operations. Empirical evidence shows that state-of-the-art SMT solvers are not very efficient at reasoning about bit-vector formulas with multiplication. This is particularly true when multiplication operators are decomposed and represented in alternative ways in the formula.We present a pre-processing heuristic that identifies certain types of decomposed multipliers, and adds special assertions to the input formula encoding the equivalence of sub-terms to word-level multiplication. The pre-processed formulas are then solved using an SMT solver. Our experiments with three SMT solvers show that our heuristic allows several formulas to be solved quickly, while the same formulas time out without the pre-processing step.