Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
Daniela Kaufmann1, Paul Beame2, Armin Biere1,3 and Jakob Nordström4
1Johannes Kepler University Linz, Austria
2University of Washington, Seattle, WA, USA
3Albert-Ludwigs-University Freiburg, Germany
4University of Copenhagen, Denmark & Lund University, Sweden
ABSTRACT
Algebraic reasoning has proven to be one of the most effective approaches for verifying gate-level integer multipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this paper that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate.
