×

zbMATH — the first resource for mathematics

Incremental column-wise verification of arithmetic circuits using computer algebra. (English) Zbl 07307313
Summary: Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is reduced by a Grö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 Gröbner basis. We also present a new technical theorem which allows to rewrite local parts of the Gröbner basis. Optimizing the Grö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 specification. Our experiments show that regular multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. We discuss in detail our complete verification approach including all optimizations.
MSC:
68 Computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Agnarsson S, Kandri-Rody A, Kapur D, Narendran P, Saunders B (1984) Complexity of testing whether a polynomial ideal is nontrivial. In: 3rd MACSYMA user’s conference, pp 452-458
[2] Beame P, Liew V (2017) Towards verifying nonlinear integer arithmetic. In: CAV, volume 10427 of LNCS. Springer, pp 238-258
[3] Berkeley Logic Synthesis and Verification Group. ABC: a system for sequential synthesis and verification. http://www.eecs.berkeley.edu/ alanmi/abc/. Bitbucket Version 1.01, last change 27 Feb 2017
[4] Biere A (2016) Collection of combinational arithmetic miters submitted to the SAT Competition 2016. In: SAT Competition 2016, volume B-2016-1 of Department of Computer Science Series of Publications B. University of Helsinki, pp 65-66
[5] Biere A (2016) Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In: Proceedings of SAT Competition 2016—solver and benchmark descriptions. University of Helsinki, pp 44-45
[6] Biere A Weaknesses of CDCL solvers. http://www.fields.utoronto.ca/talks/weaknesses-cdcl-solvers, August 2016
[7] Biere A, Heljanko K, Wieringa S (2011) AIGER 1.9 and beyond. Technical report, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria
[8] Biere A, Kauers M, Ritirc D (2017) Challenges in verifying arithmetic circuits using computer algebra. In: SYNASC. IEEE Computer Society, pp 9-15
[9] Bryant, R., Graph-based algorithms for boolean function manipulation, IEEE Trans Comput, 35, 8, 677-691 (1986) · Zbl 0593.94022
[10] Bryant, R.; Chen, Y., Verification of arithmetic circuits using binary moment diagrams, STTT, 3, 2, 137-155 (2001) · Zbl 1002.68588
[11] Buchberger B (1965) Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Ph.D. thesis, University of Innsbruck · Zbl 1245.13020
[12] Buchberger, B.; Kauers, M., Gröbner basis, Scholarpedia, 5, 10, 7763 (2010)
[13] Chen J, Chen Y (2001) Equivalence checking of integer multipliers. In: Goto S (ed) ASP-DAC 2001, pp 169-174
[14] Chen Y, Bryant R (1995) Verification of arithmetic circuits with binary moment diagrams. In: DAC, pp 535-541
[15] Ciesielski M, Yu C, Brown W, Liu D, Rossi A (2015) Verification of gate-level arithmetic circuits by function extraction. In: DAC. ACM, pp 52:1-52:6
[16] Cox, D.; Little, J.; O’Shea, D., Ideals, varieties, and algorithms (1997), New York: Springer, New York
[17] Decker W, Greuel G-M, Pfister G, Schönemann H (2016) Singular 4-1-0. http://www.singular.uni-kl.de. Accessed Jan 2018
[18] Eén N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: SAT, volume 3569 of LNCS. Springer, pp 61-75 · Zbl 1128.68463
[19] Homma, N.; Watanabe, Y.; Aoki, T.; Higuchi, T., Formal design of arithmetic circuits based on arithmetic description language, IEICE Trans, 89-A, 12, 3500-3509 (2006)
[20] Järvisalo, M.; Biere, A.; Heule, M., Simulating circuit-level simplifications on CNF, J Autom Reason, 49, 4, 583-619 (2012) · Zbl 1267.94144
[21] Kandri-Rody A, Kapur D, Narendran P (1985) An ideal-theoretic approach to work problems and unification problems over finitely presented commutative algebras. In: RTA, volume 202 of LNCS. Springer, pp 345-364 · Zbl 0581.68039
[22] Koren, I., Computer arithmetic algorithms (2001), Natick: A. K. Peters Ltd, Natick · Zbl 0994.68186
[23] Kuehlmann, A.; Paruthi, V.; Krohm, F.; Ganai, M., Robust boolean reasoning for equivalence checking and functional property verification, IEEE TCAD, 21, 12, 1377-1394 (2002)
[24] Lv, J.; Kalla, P.; Enescu, F., Efficient Gröbner basis reductions for formal verification of Galois field arithmetic circuits, IEEE TCAD, 32, 9, 1409-1420 (2013)
[25] Niemetz, A.; Preiner, M.; Biere, A., Boolector 2.0 system description, JSAT, 9, 53-58 (2014)
[26] Parhami, B., Computer arithmetic: algorithms and hardware designs (2000), Oxford: Oxford University Press, Oxford
[27] Pruss T, Kalla P, Enescu F (2014) Equivalence verification of large Galois field arithmetic circuits using word-level abstraction via Gröbner bases. In: DAC. ACM, pp 152:1-152:6
[28] Ritirc D, Biere A, Kauers M (2017) Column-wise verification of multipliers using computer algebra. In: Stewart D, Weissenbacher G (eds) FMCAD. IEEE, pp 23-30
[29] Ritirc D, Biere A, Kauers M (2018) Improving and extending the algebraic approach for verifying gate-level multipliers. In: DATE. IEEE, pp 1556-1561
[30] Sayed-Ahmed A, Große D, Kühne U, Soeken M, Drechsler R (2016) Formal verification of integer multipliers by combining Gröbner basis with logic reduction. In: DATE. IEEE, pp 1048-1053
[31] Sayed-Ahmed A, Große D, Soeken M, Drechsler R (2016) Equivalence checking using Gröbner bases. In: FMCAD. IEEE, pp 169-176
[32] Stoffel, D.; Kunz, W., Equivalence checking of arithmetic circuits on the arithmetic bit level, IEEE TCAD, 23, 5, 586-597 (2004)
[33] Wienand O, Wedler M, Stoffel D, Kunz W, Greuel G (2008) An algebraic approach for proving data correctness in arithmetic data paths. In: CAV, volume 5123 of LNCS. Springer, pp 473-486 · Zbl 1155.68448
[34] Wolfram Research, Inc. Mathematica, 2016. Version 10.4
[35] Yu, C.; Brown, W.; Liu, D.; Rossi, A.; Ciesielski, M., Formal verification of arithmetic circuits by function extraction, IEEE TCAD, 35, 12, 2131-2142 (2016)
[36] Yu, C.; Ciesielski, M.; Mishchenko, A., Fast algebraic rewriting based on and-inverter graphs, IEEE TCAD, PP, 99, 1 (2017)
[37] Yu C, Ciesielski MJ (2017) Efficient parallel verification of Galois field multipliers. In: ASP-DAC. IEEE, pp 238-243
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.