Daniela Kaufmann, Armin Biere, Manuel Kauers,
"SAT, Computer Algebra, Multipliers"
, in Laura Kovács and Andrei Voronkov: Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops, Serie EPiC Series in Computing, Vol. 71, Seite(n) 1-18, 3-2020
SAT, Computer Algebra, Multipliers
Sprache des Titels:
Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
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.