Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra

Abstract

Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice is still considered to be challenging. One of the currently most successful verification techniques relies on algebraic reasoning. In this article, we present AMulet2, a fully automatic tool for verification of integer multipliers combining SAT solving and computer algebra. Our tool models multipliers given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases. Finally, it uses a polynomial reduction algorithm to verify the correctness of the given circuit. AMulet2 is a re-factorization and improved re-implementation of our previous verification tool AMulet1 and cannot only be used as a stand-alone tool but also serves as a polynomial reasoning framework. We present a novel XOR-based slicing approach and discuss improvements on the data structures including monomial sharing.