Daniela Kaufmann, Armin Biere, Manuel Kauers,
"Incremental column-wise verification of arithmetic circuits using computer algebra"
, in Formal Methods in System Design, Springer, 2019, ISSN: 0925-9856
Original Titel:
Incremental column-wise verification of arithmetic circuits using computer algebra
Sprache des Titels:
Englisch
Original Kurzfassung:
Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most e?ective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level speci?cation is reduced by a Gro¨bner basis which is implied by the gate-level representation of the circuit. This reduction returns zero if and only if the circuit is correct. We give a rigorous formalization of this approach including soundness and completeness arguments. Furthermore we present a novel incremental column-wise technique to verify gate-level multipliers. This approach is further improved by extracting full- and half-adder constraints in the circuit which allows to rewrite and reduce the Gro¨bner basis. We also present a new technical theorem which allows to rewrite local parts of the Gro¨bner basis. Optimizing the Gro¨bner basis reduces computation time substantially. In addition we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level speci?cation. Our experiments show that regular multipliers can be veri?ed e?ciently by using o?-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. We discuss in detail our complete veri?cation approach including all optimizations.
Forschungs-