Verifying Large Multipliers by Combining SAT and Computer Algebra

We combine SAT and computer algebra to substantially improve the most effective approach for automatically verifying integer multipliers. In our approach complex final stage adders are detected and replaced by simple adders. These simplifiedmultipliersareverifiedbycomputeralgebratechniques and correctness of the replacement step by SAT solvers. Our new dedicated reduction engine relies on a Gr¨obner basis theory for coefficient rings which in contrast to previous work no longer are required to be fields. Modular reasoning allows us to verify not only large unsigned and signed multipliers much more efficiently but also truncated multipliers. We are further able to generate and check proofs an order of magnitude faster than in our previouswork,relativetoverificationtime,whileothercompeting approaches do not provide certificates.