Abstract
AMulet 2.0 is a fully automatic tool for the verification of integer multipliers using computer algebra. Our tool models multiplier circuits given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases. Finally it uses a polynomial reduction algorithm to verify the correctness of the given circuit. AMulet 2.0 is a re-factorization and improved re-implementation of our previous multiplier verification tool AMulet 1.0.
This work is supported by the LIT AI Lab funded by the State of Upper Austria.
Chapter PDF
Similar content being viewed by others
References
P. Beame, R. Impagliazzo, J. Krajícek, T. Pitassi, and P. Pudlák. Lower Bounds on Hilbert’s Nullstellensatz and Propositional Proofs. In Proc. London Math. Society, volume s3-73, pages 1–26, 1996.
T. Becker, V. Weispfenning, and H. Kredel. Gröbner Bases, volume 141 of Graduate texts in mathematics. Springer, 1993.
A. Biere. Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016. In SAT Competition 2016, volume B-2016-1 of Dep. of Computer Science Report Series B, pages 65–66. University of Helsinki, 2016.
A. Biere, K. Fazekas, M. Fleury, and M. Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Dep. of Computer Science Report Series B, pages 51–53. University of Helsinki, 2020.
A. Biere, K. Heljanko, and S. Wieringa. AIGER 1.9 And Beyond. Technical report, FMV Reports Series, JKU Linz, Austria, 2011.
R. E. Bryant and Y. Chen. Verification of arithmetic circuits using binary moment diagrams. STTT, 3(2), 137–155, 2001.
M. J. Ciesielski, T. Su, A. Yasin, and C. Yu. Understanding Algebraic Rewriting for Arithmetic Circuit Verification: a Bit-Flow Model. IEEE TCAD, pages 1–1, 2019. Early acces.
M. Clegg, J. Edmonds, and R. Impagliazzo. Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability. In STOC 1996, pages 174–183. ACM, 1996.
D. Cox, J. Little, and D. O’Shea. Ideals, Varieties, and Algorithms. Springer-Verlag, New York, 1997.
T. Granlund and the GMP development team. GNU MP: The GNU Multiple Precision Arithmetic Library, 2016. Version 6.1.2.
E. Hirsch, D. Itsykson, A. Kojevnikov, E. Kulikov, and S. Nikolenko. Report on the Mixed Boolean-Algebraic Solver. Technical report, Laboratory of Mathematical Logic of St. Petersburg Dep. of Steklov Institute of Mathematics, 2005.
N. Homma, Y. Watanabe, T. Aoki, and T. Higuchi. Formal Design of Arithmetic Circuits Based on Arithmetic Description Language. IEICE Transactions, 89-A(12):3500–3509, 2006.
D. Kaufmann. Amulet 1.5. https://github.com/d-kfmnn/amulet, 2020.
D. Kaufmann. Artifact for AMulet2.0 for verifying multiplier circuits. http://fmv.jku.at/amulet2_artifact, 2020.
D. Kaufmann. Formal Verification of Multiplier Circuits using Computer Algebra. PhD thesis, Informatik, Johannes Kepler University Linz, 2020.
D. Kaufmann and A. Biere. Nullstellensatz-proofs for multiplier verification. In Computer Algebra in Scientific Computing, volume 12291 of LNCS, pages 368–389. Springer, 2020.
D. Kaufmann, A. Biere, and M. Kauers. Verifying Large Multipliers by Combining SAT and Computer Algebra. In FMCAD 2019, pages 28–36. IEEE, 2019.
D. Kaufmann, A. Biere, and M. Kauers. Incremental Column-wise verification of arithmetic circuits using computer algebra. Formal Methods Syst. Des., 56(1):22–54, 2020.
D. Kaufmann, A. Biere, and M. Kauers. SAT, Computer Algebra, Multipliers. In Vampire 2018 and Vampire 2019, volume 71 of EPiC Series in Computing, pages 1–18. EasyChair, 2020.
D. Kaufmann, M. Fleury, and A. Biere. Pacheck and Pastèque, Checking Practical Algebraic Calculus Proofs. In FMCAD 2020, volume 1 of FMCAD, pages 264–269. TU Vienna Academic Press, 2020.
D. Kaufmann, M. Kauers, A. Biere, and D. Cok. Arithmetic Verification Problems Submitted to the SAT Race 2019. In SAT Race 2019, volume B-2019-1 of Dep. of Computer Science Report Series B, page 49. University of Helsinki, 2019.
A. Kuehlmann, V. Paruthi, F. Krohm, and M. Ganai. Robust Boolean reasoning for equivalence checking and functional property verification. IEEE TCAD, 21(12), 1377–1394, 2002.
J. Lv, P. Kalla, and F. Enescu. Efficient Gröbner Basis Reductions for Formal Verification of Galois Field Arithmetic Circuits. IEEE TCAD, 32(9):1409–1420, 2013.
A. Mahzoon, D. Große, and R. Drechsler. PolyCleaner: Clean your Polynomials before Backward Rewriting to verify Million-gate Multipliers. In ICCAD 2018, pages 129:1–129:8. ACM, 2018.
A. Mahzoon, D. Große, and R. Drechsler. RevSCA: Using Reverse Engineering to Bring Light into Backward Rewriting for Big and Dirty Multipliers. In DAC 2019, pages 185:1–185:6. ACM, 2019.
A. Mahzoon, D. Große, C. Scholl, and R. Drechsler. Towards formal verification of optimized and industrial multipliers. In DATE, pages 544–549. IEEE, 2020.
B. Parhami. Computer Arithmetic - Algorithms and Hardware designs. Oxford University Press, 2000.
H. Sharangpani and M. L. Barton. Statistical analysis of floating point flaw in the pentium processor. 1994.
M. Temel, A. Slobodová, and W. A. Hunt. Automated and scalable verification of integer multipliers. In CAV (1), volume 12224 of Lecture Notes in Computer Science, pages 485–507. Springer, 2020.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Kaufmann, D., Biere, A. (2021). AMulet 2.0 for Verifying Multiplier Circuits. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12652. Springer, Cham. https://doi.org/10.1007/978-3-030-72013-1_19
Download citation
DOI: https://doi.org/10.1007/978-3-030-72013-1_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72012-4
Online ISBN: 978-3-030-72013-1
eBook Packages: Computer ScienceComputer Science (R0)