Daniela Ritirc, Armin Biere, Manuel Kauers,
"Improving and Extending the Algebraic Approach for Verifying Gate-Level Multipliers"
: Proc. Design, Automation and Test in Europe (DATE'18), Seite(n) 1556-1561, 3-2018
Improving and Extending the Algebraic Approach for Verifying Gate-Level Multipliers
Sprache des Titels:
Proc. Design, Automation and Test in Europe (DATE'18)
The currently most effective approach for verifying gate-level multipliers uses Computer Algebra. It reduces a wordlevel multiplier speci?cation by a Gr¨obner 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¨obner basis, which speeds up computation substantially. Refactoring the speci?cation 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 speci?cation.