Document Open Access Logo

Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification

Authors Clemens Hofstadler , Daniela Kaufmann

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CP.2025.14.pdf
  • Filesize: 1.1 MB
  • 22 pages
HTML5 Logo HTML (experimental)
LIPIcs.CP.2025.14.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Computer Algebra
  • FGLM
  • And-Inverter Graphs
  • Hardware Verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Formal verification of arithmetic circuits using computer algebra has been shown to be highly successful. The circuit is encoded as a system of polynomials, which automatically generates a lexicographic Gröbner basis. Correctness is then verified by computing the polynomial remainder of the specification. To optimize the remainder computation, prior work extracts linear polynomials. However, this required recomputing a Gröbner basis with respect to a degree-compatible order.
In this paper, we show that this computationally expensive step is unnecessary and propose a novel hybrid verification approach that combines an FGLM-style linearization technique with a guess-and-prove method using SAT solving to derive the linear relations directly from lexicographic Gröbner bases. We enhance our approach using caching techniques and propagating vanishing monomials. Our experimental results demonstrate that our method significantly outperforms previous linearization techniques.

Cite As Get BibTex

Clemens Hofstadler and Daniela Kaufmann. Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.14

Author Details

Clemens Hofstadler
  • Johannes Kepler University, Linz, Austria
Daniela Kaufmann
  • TU Wien, Austria

Funding

  • Hofstadler, Clemens: LIT AI Lab funded by the state of Upper Austria.
  • Kaufmann, Daniela: Austrian Science Fund (FWF) [10.55776/ESP666].

Acknowledgements

We thank Jérémy Berthomieu and the reviewers for insightful comments.

Supplementary Materials

References

  1. Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. http://www.eecs.berkeley.edu/~alanmi/abc/, 2019. Bitbucket Version 1.01.
  2. Jérémy Berthomieu, Christian Eder, and Mohab Safey El Din. msolve: A library for solving polynomial systems. In Intl. Symposium on Symbolic and Algebraic Computation (ISSAC), pages 51-58. ACM, 2021. URL: https://doi.org/10.1145/3452143.3465545.
  3. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024. In Proc. of SAT Competition 2024 - Solver, Benchmark and Proof Checker Descriptions, volume B-2024-1 of Department of Computer Science Report Series B, pages 8-10. University of Helsinki, 2024. Google Scholar
  4. Bruno Buchberger. Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, University of Innsbruck, 1965. Google Scholar
  5. David A. Cox, John Little, and Donal O'Shea. Ideals, varieties, and algorithms - an introduction to computational algebraic geometry and commutative algebra (2. ed.). Undergraduate texts in mathematics. Springer, 1997. Google Scholar
  6. David A. Cox, John Little, and Donal O'Shea. Using Algebraic Geometry. Springer, 2005. Google Scholar
  7. Jo Devriendt, Stephan Gocht, Emir Demirovic, Jakob Nordström, and Peter J. Stuckey. Cutting to the core of pseudo-boolean optimization: Combining core-guided search with cutting planes reasoning. In Conf. on Artificial Intelligence AAAI, pages 3750-3758. AAAI Press, 2021. URL: https://doi.org/10.1609/aaai.v35i5.16492.
  8. Jean-Charles Faugère, Patrizia M. Gianni, Daniel Lazard, and Teo Mora. Efficient computation of zero-dimensional gröbner bases by change of ordering. J. Symb. Comput., 16(4):329-344, 1993. URL: https://doi.org/10.1006/jsco.1993.1051.
  9. Clemens Hofstadler and Daniela Kaufmann. TalisMan. Software, version 1.0., swhId: https://archive.softwareheritage.org/swh:1:dir:8af022a61661d2b7fb281abbdc2f18d51f221c20;origin=https://github.com/d-kfmnn/talisman;visit=swh:1:snp:d83634ac4675c6c2a76a146bbea12568e3c642a1;anchor=swh:1:rev:be8187df3d18d3530bd175136d6865269cbc21e2 (visited on 2025-07-16). URL: https://github.com/d-kfmnn/talisman/tree/be8187d, URL: https://doi.org/10.4230/artifacts.23376.
  10. Naofumi Homma, Yuki Watanabe, Takafumi Aoki, and Tatsuo Higuchi. Formal design of arithmetic circuits based on arithmetic description language. IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 89-A(12):3500-3509, 2006. URL: https://doi.org/10.1093/ietfec/e89-a.12.3500.
  11. Daniela Kaufmann. Formal Verification of Multiplier Circuits using Computer Algebra. PhD thesis, Computer Science, Johannes Kepler University Linz, 2020. Google Scholar
  12. Daniela Kaufmann, Paul Beame, Armin Biere, and Jakob Nordström. Adding dual variables to algebraic reasoning for gate-level multiplier verification. In 2Design, Automation & Test in Europe Conf. & Exhibition, DATE, pages 1431-1436. IEEE, 2022. URL: https://doi.org/10.23919/DATE54114.2022.9774587.
  13. Daniela Kaufmann and Jérémy Berthomieu. Extracting linear relations from gröbner bases for formal verification of and-inverter graphs. In Tools and Algorithms for the Construction and Analysis of Systems TACAS, volume 15696 of LNCS, pages 355-374. Springer, Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90643-5_19.
  14. Daniela Kaufmann and Armin Biere. Amulet 2.0 for verifying multiplier circuits. In Tools and Algorithms for the Construction and Analysis of Systems TACAS, volume 12652 of LNCS, pages 357-364. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_19.
  15. Daniela Kaufmann, Armin Biere, and Manuel Kauers. Verifying large multipliers by combining SAT and computer algebra. In Formal Methods in Computer Aided Design, FMCAD, pages 28-36. IEEE, 2019. URL: https://doi.org/10.23919/FMCAD.2019.8894250.
  16. Daniela Kaufmann, Armin Biere, and Manuel Kauers. Incremental column-wise verification of arithmetic circuits using computer algebra. Formal Methods Syst. Des., 56(1):22-54, 2020. URL: https://doi.org/10.1007/s10703-018-00329-2.
  17. Alexander Konrad and Christoph Scholl. Symbolic computer algebra for multipliers revisited - it’s all about orders and phases. In Formal Methods in Computer-Aided Design FMCAD, pages 261-271. IEEE, 2024. URL: https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_32.
  18. Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, and Rolf Drechsler. Divider verification using symbolic computer algebra and delayed don't care optimization. In Formal Methods in Computer-Aided Design FMCAD, pages 1-10. IEEE, 2022. URL: https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_17.
  19. Andreas Kuehlmann, Viresh Paruthi, Florian Krohm, and Malay K. Ganai. Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 21(12):1377-1394, 2002. URL: https://doi.org/10.1109/TCAD.2002.804386.
  20. Jinpeng Lv, Priyank Kalla, and Florian Enescu. Efficient gröbner basis reductions for formal verification of galois field arithmetic circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 32(9):1409-1420, 2013. URL: https://doi.org/10.1109/TCAD.2013.2259540.
  21. Alireza Mahzoon, Daniel Große, and Rolf Drechsler. Polycleaner: clean your polynomials before backward rewriting to verify million-gate multipliers. In Intl. Conf. on Computer-Aided Design ICCAD, page 129. ACM, 2018. URL: https://doi.org/10.1145/3240765.3240837.
  22. Alireza Mahzoon, Daniel Große, Christoph Scholl, and Rolf Drechsler. Towards formal verification of optimized and industrial multipliers. In Design, Automation & Test in Europe Conf. & Exhibition, DATE, pages 544-549. IEEE, 2020. URL: https://doi.org/10.23919/DATE48585.2020.9116485.
  23. Tobias Philipp and Peter Steinke. Pblib - A library for encoding pseudo-boolean constraints into CNF. In Theory and Applications of Satisfiability Testing - SAT 2015 - 18th Intl. Conf., Austin, TX, USA, September 24-27, 2015, Proceedings, volume 9340 of LNCS, pages 9-16. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_2.
  24. William A. Stein. Modular Forms: A Computational Approach, volume 79. American Mathematical Soc., 2007. Google Scholar
  25. Mertcan Temel. Vescmul: Verified implementation of s-c-rewriting for multiplier verification. In Tools and Algorithms for the Construction and Analysis of Systems TACAS, volume 14570 of LNCS, pages 340-349. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_19.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact