Improving and Extending the Algebraic Approach for Verifying Gate‐Level Multipliers

Daniela Ritirca, Armin Biereb and Manuel Kauersc
Johannes Kepler University Linz, Altenbergerstr. Linz, Austria
adaniela.ritirc@jku.at
barmin.biere@jku.at
cmanuel.kauers@jku.at

ABSTRACT


The currently most effective approach for verifying gate‐level multipliers uses Computer Algebra. It reduces a word level multiplier specification by a Gröbner basis derived from a gate‐level implementation. This reduction produces zero if and only if the circuit is a multiplier. We improve this approach by extracting full‐ and half‐adder constraints to reduce the Gröbner basis, which speeds up computation substantially. Refactoring the specification in terms of partial products instead of inputs yields further improvements. As a third contribution we extend these algebraic techniques to verify the equivalence of bit‐level multipliers without using a word‐level specification.



Full Text (PDF)