Daniela Ritirc, Armin Biere, Manuel Kauers,
"Column-Wise Verification of Multipliers Using Computer Algebra"
: Proc. 17th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17), 2017
Column-Wise Verification of Multipliers Using Computer Algebra
Sprache des Titels:
Proc. 17th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17)
Verifying arithmetic circuits, and most prominently multipliers, is an important problem but in practice still requires substantial manual effort. Recent work tries to solve this issue using techniques from computer algebra. The most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this paper we give a rigorous formalization of this approach and present a new column-wise veri?cation technique forthecorrectnessofgate-levelmultiplierswhichdoesnotrequire the reduction of a full word-level speci?cation. We formally prove soundness and completeness of our technique, making use of our precise formalization. Our experiments show that simple multipliers can be veri?ed ef?ciently by using off-theshelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. Further, our paperindependentlycon?rmstheeffectivenessofpreviousrelated work. We make all benchmarks and tools publicly available.