Daniela Kaufmann, Armin Biere, Manuel Kauers,
"Verifying Large Multipliers by Combining SAT and Computer Algebra"
, in Clark Barrett and Jin Yang: Proc. 19th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19), FMCAD Inc, Seite(n) 28-36, 10-2019, ISBN: 978-0-9835678-9-9
Verifying Large Multipliers by Combining SAT and Computer Algebra
Sprache des Titels:
Proc. 19th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19)
We combine SAT and computer algebra to substantially improve the most effective approach for automatically verifying integer multipliers. In our approach complex ?nal stage adders are detected and replaced by simple adders. These simpli?edmultipliersareveri?edbycomputeralgebratechniques and correctness of the replacement step by SAT solvers. Our new dedicated reduction engine relies on a Gr¨obner basis theory for coef?cient rings which in contrast to previous work no longer are required to be ?elds. Modular reasoning allows us to verify not only large unsigned and signed multipliers much more ef?ciently but also truncated multipliers. We are further able to generate and check proofs an order of magnitude faster than in our previouswork,relativetoveri?cationtime,whileothercompeting approaches do not provide certi?cates.