SAT, Computer Algebra, Multipliers

Verifying multiplier circuits is an important problem which in practice still requires substantialmanual effort. The currently most effective approach uses polynomial reasoning. However parts of amultiplier, i.e., complex final stage adders are hard to verify using computer algebra. In our approachwe combine SAT and computer algebra to substantially improve automated verification of integermultipliers. In this paper we focus on the implementation details of our new dedicated reductionengine, which not only allows fully automated adder substitution, but also employs polynomial re-duction efficiently. Our tool is furthermore able to generate proof certificates in the practical algebraiccalculus and we also investigate the size of these proofs for one specific multiplier architecture.