Verifying Large Multipliers by Combining SAT and Computer Algebra
Sprache des Vortragstitels:
Sprache des Tagungstitel:
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.