×

Formal verification of integer multiplier circuits using algebraic reasoning: a survey. (English) Zbl 07410738

Drechsler, Rolf (ed.) et al., Recent findings in Boolean techniques. Selected papers from the 14th international workshop on Boolean problems, IWSBP, virtual, September 24–25, 2020. Cham: Springer. 1-27 (2021).
Summary: Digital circuits are extensively used in computers and digital systems and it is of high importance to guarantee that these circuits are correct in order to prevent issues like the famous Pentium FDIV bug. Formal verification can be used to derive the correctness of a given circuit with respect to a certain specification. However arithmetic circuits, and most prominently multipliers, impose a challenge for existing verification techniques. Currently one of the most effective techniques is based on algebraic reasoning. In this approach the circuit is modeled as a set of pseudo-Boolean polynomials and the word-level specification is reduced by a Gröbner basis, which is implied by the polynomial representation of the circuit. The circuit is correct if and only if the final result is zero. Nonetheless the verification process might not be error-free. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. In this paper we survey the current state of the art of this work. We give an overview over recent solving techniques, available benchmarks, and include a comprehensive evaluation.
For the entire collection see [Zbl 1470.94002].

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68Q06 Networks and circuits as models of computation; circuit complexity

Software:

EPFL
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Amarú, L., Gaillardon, P.-E., De Micheli, G.: The EPFL combinational benchmark suite. In: International Workshop on Logic and Synthesis (IWLS), pp. 57-61 (2015)
[2] Amarú, L., Gaillardon, P.-E., De Micheli, G.: The EPFL combinational benchmark suite (2020). https://www.epfl.ch/labs/lsi/page-102566-en-html/benchmarks/
[3] Amarú, L., Gaillardon, P.-E., De Micheli, G.: The EPFL combinational benchmark suite (2020). https://github.com/lsils/benchmarks
[4] Beame, P., Impagliazzo, R., Krajícek, J., Pitassi, T., Pudlák, P.: Lower Bounds on Hilbert’s Nullstellensatz and Propositional Proofs. In: Proceedings of the London Mathematical Society, vol. s3-73, pp. 1-26 (1996) · Zbl 0853.03017
[5] Beame, P., Liew, V.: Towards Verifying Nonlinear Integer Arithmetic. In: Proceedings of the International Conference on Computer Aided Verification (CAV) 2017. LNCS, vol. 10427, pp. 238-258. Springer, New York (2017)
[6] Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification (2019). http://www.eecs.berkeley.edu/ alanmi/abc/. Bitbucket Version 1.01
[7] Biere, A.: Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016. In: SAT Competition 2016. Department of Computer Science Report Series B, vol. B-2016-1, pp. 65-66. University of Helsinki, Helsinki (2016)
[8] Biere, A.: Weaknesses of CDCL solvers, August 2016. In: Fields Institute Workshop on Theoretical Foundations of SAT Solving. http://www.fields.utoronto.ca/talks/weaknesses-cdcl-solvers
[9] Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Proceedings of the SAT Competition 2020—Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51-53. University of Helsinki, Helsinki (2020)
[10] Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Comput. 35(8), 677-691 (1986) · Zbl 0593.94022
[11] Bryant, R.E., Chen, Y.: Verification of arithmetic circuits using binary moment diagrams. STTT 3(2), 137-155 (2001) · Zbl 1002.68588
[12] Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal, PhD thesis. University of Innsbruck, Innsbruck (1965) · Zbl 1245.13020
[13] Chen, Y., Bryant, R.E.: Verification of Arithmetic Circuits with Binary Moment Diagrams. In: Design Automation Conference, DAC 1995, pp. 535-541. ACM, New York (1995)
[14] Chen, Y., Clarke, E., Ho, P., Hoskote, Y., Kam, T., Khaira, M., O’Leary, J., Zhao, X.: Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking. In: FMCAD 1996. LNCS, vol. 1166, pp. 19-33. Springer, Berlin (1996)
[15] Ciesielski, M.J., Yu, C., Brown, W., Liu, D., Rossi, A.: Verification of Gate-level Arithmetic Circuits by Function Extraction. In: Design Automation Conference, DAC 2015, pp. 52:1-52:6. ACM, New York (2015)
[16] Ciesielski, M.J., Su, T., Yasin, A., Yu, C.: Understanding algebraic rewriting for arithmetic circuit verification: a Bit-Flow model. IEEE TCAD, pp. 1-1 (2019). Early acces
[17] Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: STOC 1996, pp. 174-183. ACM, New York (1996) · Zbl 0938.68825
[18] Cox, D., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms. Springer, New York (1997)
[19] Heule, M.J.H., Biere, A.: Proofs for satisfiability problems. In: All about Proofs, Proofs for All Workshop, APPA 2014, vol. 55, pp. 1-22. College Publications, Australia (2015) · Zbl 1431.03024
[20] 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)
[21] Homma Laboratory, RIEC, Tohoku University. Arithmetic Module Generator. https://www.ecsis.riec.tohoku.ac.jp/topics/amg/
[22] Hunt, W.A., Jr., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. Philos. Trans. Royal Soc. A 375(2104), 20150399 (2017)
[23] Kaufmann, D.: AMulet 1.5 (2020). https://github.com/d-kfmnn/amulet
[24] Kaufmann, D.: Formal Verification of Multiplier Circuits using Computer Algebra. PhD thesis, Informatik, Johannes Kepler University Linz (2020)
[25] Kaufmann, D., Biere, A.: Nullstellensatz-proofs for multiplier verification. In: CASC. Lecture Notes in Computer Science. Springer, Berlin (2020, to appear)
[26] Kaufmann, M., Moore, J.S.: ACL2 Version 8.2 (2019). http://www.cs.utexas.edu/users/moore/acl2/
[27] Kaufmann, D., Biere, A., Kauers, M.: Incremental Column-wise verification of arithmetic circuits using computer algebra. In: Formal Methods in System Design (2019). Online first · Zbl 07307313
[28] Kaufmann, D., Biere, A., Kauers, M.: Verifying Large Multipliers by Combining SAT and Computer Algebra. In: FMCAD 2019, pp. 28-36. IEEE, New York (2019)
[29] Kaufmann, D., Kauers, M., Biere, A., Cok, D.: Arithmetic Verification Problems Submitted to the SAT Race 2019. In: SAT Race 2019. Department of Computer Science Report Series B, vol. B-2019-1, p. 49. University of Helsinki, Helsinki (2019)
[30] Kaufmann, D., Fleury, M., Biere, A.: Pacheck and Pastèque, Checking Practical Algebraic Calculus Proofs. In: FMCAD 2020. FMCAD, vol. 1, pp. 264-269. TU Vienna Academic Press, Austria (2020)
[31] 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)
[32] Liew, V., Beame, P., Devriendt, J., Elffers, J., Nordström, J.: Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning. In: FMCAD 2020. FMCAD, vol. 1, pp. 194-204. TU Vienna Academic Press, Austria (2020)
[33] Lv, J., Kalla, P.: Formal Verification of Galois Field Multipliers Using Computer Algebra Techniques. In: International Conference on VLSI Design, VLSID 2012, pp. 388-393. IEEE Computer Society, New York (2012)
[34] 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)
[35] Mahzoon, A., Große, D., Drechsler, R.: GenMul (2018). http://sca-verification.org/genmul
[36] Mahzoon, A., Große, D., Drechsler R.: GenMul (2018). https://github.com/amahzoon/genmul
[37] Mahzoon, A., Große, D., Drechsler, R.: PolyCleaner (2018). http://sca-verification.org/polycleaner
[38] Mahzoon, A., Große, D., Drechsler, R.: PolyCleaner: clean your polynomials before backward rewriting to verify Million-gate Multipliers. In: ICCAD 2018, pp. 129:1-129:8. ACM, New York (2018)
[39] Mahzoon, A., Große, D., Drechsler, R.: RevSCA and RevSCA-2.0 (2019). http://sca-verification.org/revsca
[40] Mahzoon, A., Große, D., Drechsler, R.: RevSCA: using reverse engineering to bring light into backward rewriting for big and dirty multipliers. In: DAC 2019, pp. 185:1-185:6. ACM, New York (2019)
[41] Mahzoon, A., Große, D., Scholl, C., Drechsler, R.: DyPoSub (2020). http://sca-verification.org/dyposub
[42] Mahzoon, A., Große, C. Scholl, D., Drechsler, R.: Towards formal verification of optimized and industrial multipliers. In: DATE, pp. 544-549. IEEE, New York (2020)
[43] Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector 3.0. In: CAV 2018. LNCS, vol. 10981, pp. 587-595. Springer, Berlin (2018)
[44] Parhami, B.: Computer Arithmetic—Algorithms and Hardware designs. Oxford University, Oxford (2000)
[45] Pavlenko, E., Wedler, M., Stoffel, D., Kunz, W., Wienand, O., Karibaev, E.: Modeling of custom-designed arithmetic components for ABL normalization. In: Forum on Specification and Design Languages, FDL 2008, pp. 124-129. IEEE, New York (2008) · Zbl 1160.68666
[46] Ritirc, D., Biere, A., Kauers, M.: A practical polynomial calculus for arithmetic circuit verification. In: SC2 2018, pp. 61-76. CEUR-WS (2018)
[47] Sentovich, E., Singh, K., Lavagno, L., Moon, C., Murgai, R., Saldanha, A., Savoj, H., Stephan, P., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: SIS. https://ptolemy.berkeley.edu/projects/embedded/pubs/downloads/sis/index.htm
[48] Sentovich, E., Singh, K., Lavagno, L., Moon, C., Murgai, R., Saldanha, A., Savoj, H., Stephan, P., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: SIS: a system for sequential circuit synthesis. Technical Report UCB/ERL M92/41, EECS Department, University of California, Berkeley (1992)
[49] Sharangpani, H., Barton, M.L.: Statistical Analysis of Floating Point Flaw in the Pentium Processor (1994)
[50] Stoffel, D., Kunz, W.: Equivalence checking of arithmetic circuits on the arithmetic bit level. IEEE TCAD 23(5), 586-597 (2004)
[51] Temel, M.: MultGen (2020). https://github.com/temelmertcan/multgen
[52] Temel, M., Slobodová, A., Hunt, W.A.: Automated and scalable verification of integer multipliers. In: CAV (1). Lecture Notes in Computer Science, vol. 12224, pp. 485-507. Springer, Berlin (2020) · Zbl 1478.68178
[53] Vasudevan, S., Viswanath, V., Sumners, R.W., Abraham, J.A.: Automatic verification of arithmetic circuits in RTL using stepwise refinement of term rewriting systems. IEEE Trans. Comput. 56(10), 1401-1414 (2007) · Zbl 1391.94905
[54] Wienand, O., Wedler, M., Stoffel, D., Kunz, W., Greuel, G.: An algebraic approach for proving data correctness in arithmetic data paths. In: International Conference on Computer Aided Verification, CAV 2008. LNCS, vol. 5123, pp. 473-486. Springer, Berlin (2008) · Zbl 1155.68448
[55] Wolf, C.: Yosys Open SYnthesis Suite. http://www.clifford.at/yosys/
[56] Yu, C.: Algebraic RewriTing in ABC (2018). https://github.com/ycunxi/abc
[57] Yu, C., Brown, W., Liu, D., Rossi, A., Ciesielski, M.J.: Formal verification of arithmetic circuits by function extraction. IEEE TCAD 35(12), 2131-2142 (2016)
[58] Yu, C., Ciesielski, M.J.: Efficient parallel verification of galois field multipliers. In: Asia and South Pacific Design Automation Conference, ASP-DAC 2017, pp. 238-243. IEEE, New York (2017)
[59] Yu, C., Ciesielski, M.J.: Formal analysis of Galois field arithmetic circuits-parallel verification and reverse engineering. IEEE TCAD 38(2), 354-365 (2019)
[60] Yu, C., Ciesielski, M.J., Mishchenko, A.: Fast algebraic rewriting based on and-inverter graphs
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.