Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits

Chen Chen; Clemens Hofstadler; Daniela Kaufmann

arxiv: 2603.09501 · v2 · submitted 2026-03-10 · 💻 cs.SC

Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits

Clemens Hofstadler , Daniela Kaufmann , Chen Chen This is my paper

Pith reviewed 2026-05-15 13:44 UTC · model grok-4.3

classification 💻 cs.SC

keywords algebraic verificationarithmetic circuitsmultimodular computationhomomorphic imagespolynomial rewritingcircuit verificationmultipliersword-level verification

0 comments

The pith

Verification of large arithmetic circuits can avoid arbitrary-precision arithmetic by performing polynomial rewriting modulo multiple small primes in parallel.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that word-level algebraic verification of arithmetic circuits does not require handling large integers. Instead, it uses a hybrid approach combining linear and nonlinear polynomial rewriting, but executes all steps using homomorphic images modulo different primes. These computations run in parallel across the moduli. This multimodular method is shown to be effective on multiplier circuits when implemented in TalisMan2.0. A sympathetic reader would care because growing operand sizes make big-integer operations a bottleneck in verification.

Core claim

The central claim is that hybrid algebraic verification based on polynomial reasoning, when lifted to multimodular homomorphic images computed in parallel modulo distinct primes, preserves all necessary information to verify arithmetic circuits correctly while entirely avoiding large-integer arithmetic.

What carries the argument

Multimodular reasoning via homomorphic images modulo different primes, combined with linear and nonlinear rewriting rules for polynomials.

If this is right

Verification scales to larger word sizes without the overhead of arbitrary-precision numbers.
The parallel nature of computations across primes enables faster runtimes on standard hardware.
Hybrid linear-nonlinear rewriting improves verification power over single-type approaches.
Results on multiplier benchmarks demonstrate practical speedups compared to prior methods.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar multimodular techniques could extend to verifying other types of circuits or polynomial identities beyond multipliers.
Choosing optimal sets of primes might further reduce verification time if tuned to circuit structure.
If the method preserves soundness, it could integrate into broader formal verification workflows for hardware design.

Load-bearing premise

The combination of linear and nonlinear rewriting rules stays complete and sound when applied to the homomorphic images modulo the selected primes.

What would settle it

A counterexample would be an arithmetic circuit with a bug that the multimodular verifier incorrectly reports as correct, or a correct circuit that the verifier fails to confirm due to lost information across moduli.

Figures

Figures reproduced from arXiv: 2603.09501 by Chen Chen, Clemens Hofstadler, Daniela Kaufmann.

**Figure 1.** Figure 1: AIG and polynomial encoding of a 2-bit multiplier. To enforce Boolean semantics when working over coefficient domains R 6= B, we introduce Boolean value polynomials. For each primary input xi of the AIG, we define the constraint x 2 i − xi = 0. We denote the set of all such polynomials by B(C). Boolean constraints propagate through the circuit, and it therefore suffices to introduce Boolean value polynomia… view at source ↗

**Figure 2.** Figure 2: Overview of the TalisMan2.0 workflow. Double-edged boxes are computations that are run in parallel in TalisMan2.0. pletely independent, they can be run in parallel, yielding near-linear speedups on modern multicore machines. Finally, we note that the multimodular approach also supports the computation of witnesses of faulty circuits. By Lemma 1, any counterexample discovered during verification over a mod… view at source ↗

**Figure 3.** Figure 3: Comparison of TalisMan2.0 and related work. For each tool the number of solved instances is added in parentheses. We consider two types of benchmarks: structured circuits, where the components of a multiplier (partial product generation (PPG), partial product accumulation (PPA), and the final stage adder (FSA)) are clearly separable, and synthesized circuits, where gates are merged and rewritten to optim… view at source ↗

**Figure 4.** Figure 4: Comparing the default setting when either uniform input sampling (left), only linear rewriting (middle), or only nonlinear rewriting is used (right). Name Total TalisMan2.0 — Phase Times (s) Linear Nonlinear Prepr. Extract Sample Guess* Prove* Repair* Rewrite Simplify Rewrite abc64-cmp 2.3 2.1 <0.05 <0.05 <0.05 <0.05 - <0.05 - - bp-ar-cl 44.0 1.4 0.7 0.9 9.7 26.6 3.0 0.1 <0.05 0.2 bp-ba-cn 42.0 1.6 <0.05 2… view at source ↗

read the original abstract

Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word sizes grow. In this paper, we present a hybrid algebraic verification technique based on polynomial reasoning that combines linear and nonlinear rewriting. Our approach relies on multimodular reasoning using homomorphic images, where computations are performed in parallel modulo different primes, thereby avoiding any large-integer arithmetic. We implement the proposed method in the verification tool TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The multimodular hybrid rewriting speeds up multiplier verification in practice but leaves soundness over Z unproven without a coefficient bound.

read the letter

The paper's core move is to run linear and nonlinear polynomial rewriting for arithmetic circuit verification in parallel over several small prime moduli. This keeps every number small and avoids arbitrary-precision arithmetic entirely. They built it into TalisMan2.0 and report faster runtimes than prior algebraic tools on standard multiplier benchmarks. That practical payoff is the clearest contribution: the hybrid rule set plus the parallel modular setup is a concrete implementation tweak that matters for word-level hardware checks where big integers become the bottleneck. The benchmarks look solid enough to show the speed gain is real on the circuits they tested. The main gap is soundness. Success modulo each prime only implies the difference polynomial is zero over the integers when the product of the primes exceeds the largest possible coefficient in that polynomial. The abstract gives no sign that the authors compute or enforce such a bound, so a non-zero error term divisible by all chosen primes would pass every check and produce a false positive. If the full paper supplies an explicit bound or a dynamic prime-selection step that guarantees the product is large enough, the method holds; otherwise the empirical wins rest on an unverified assumption. This work is aimed at verification engineers and tool builders who already use algebraic methods for circuits. A reader who needs faster multiplier checks will find usable ideas in the implementation and the numbers. It is worth sending to a serious referee because the technique is specific, the experiments are reproducible in principle, and the soundness question is fixable with one additional argument or check.

Referee Report

1 major / 2 minor

Summary. The paper claims a hybrid algebraic verification technique for arithmetic circuits that combines linear and nonlinear polynomial rewriting with multimodular reasoning. Computations are performed independently in parallel modulo several small primes via homomorphic images, avoiding arbitrary-precision arithmetic entirely. The method is implemented in TalisMan2.0 and evaluated on a suite of multiplier benchmarks, where it is reported to significantly outperform existing approaches.

Significance. If the soundness of the multimodular lifting is established, the technique could meaningfully improve scalability of word-level algebraic verification for large operands by keeping all intermediate arithmetic small. The reported benchmark gains on multipliers provide concrete evidence of practical utility in hardware verification tools.

major comments (1)

[multimodular reasoning section (around the hybrid rewriting algorithm)] The soundness argument for multimodular verification is incomplete. Success of the rewriting checks modulo each prime implies the difference polynomial is zero over Z only when the product of the moduli exceeds twice the maximum absolute coefficient that can appear in any relevant difference polynomial of the given degree. No coefficient bound is derived or enforced, and no explicit prime-selection criterion guaranteeing this inequality is stated (see the description of the multimodular procedure and the claim that homomorphic images preserve all necessary verification information).

minor comments (2)

[Abstract] The abstract states that the approach 'significantly improves upon existing approaches' without naming the baselines or reporting quantitative speed-up factors; adding this information would strengthen the claim.
[preliminaries / method] Notation for the set of primes and the homomorphic mapping is introduced without an explicit definition of the ring homomorphism or the precise lifting step from the modular results back to Z; a short formal statement would improve clarity.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the thorough review and insightful comments on our paper. We address the major comment regarding the soundness of the multimodular reasoning below and plan to incorporate the necessary clarifications in the revised manuscript.

read point-by-point responses

Referee: The soundness argument for multimodular verification is incomplete. Success of the rewriting checks modulo each prime implies the difference polynomial is zero over Z only when the product of the moduli exceeds twice the maximum absolute coefficient that can appear in any relevant difference polynomial of the given degree. No coefficient bound is derived or enforced, and no explicit prime-selection criterion guaranteeing this inequality is stated (see the description of the multimodular procedure and the claim that homomorphic images preserve all necessary verification information).

Authors: We acknowledge that the soundness argument in the multimodular reasoning section is indeed incomplete in its current form. To address this, we will derive an explicit upper bound on the coefficients of the difference polynomial in the revised version, taking into account the degree and the structure of the arithmetic circuit. Additionally, we will provide a clear criterion for selecting the primes such that their product is sufficiently large to ensure that vanishing modulo each prime implies the polynomial is zero over the integers. This will be added to the description of the hybrid rewriting algorithm and the multimodular procedure, thereby completing the justification that the homomorphic images preserve all necessary information for verification. revision: yes

Circularity Check

0 steps flagged

No circularity; derivation uses standard homomorphic images and modular arithmetic

full rationale

The paper's central technique combines linear/nonlinear polynomial rewriting with multimodular evaluation over homomorphic images modulo distinct primes. This rests on well-established facts from commutative algebra (polynomial ring homomorphisms and the Chinese Remainder Theorem) that are independent of the paper's specific implementation or benchmarks. No equations reduce a claimed result to a fitted parameter, self-referential definition, or ansatz imported only via self-citation. The method is presented as a direct application of these external properties to avoid big-integer arithmetic, with evaluation on multiplier benchmarks serving as empirical support rather than a definitional loop. The derivation chain is therefore self-contained against external mathematical benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on standard algebraic properties of polynomial rings and modular homomorphisms with no new free parameters or invented entities.

axioms (2)

standard math Polynomial rings over the integers admit homomorphic images modulo distinct primes that preserve ring operations
Invoked to justify performing verification computations in parallel modulo different primes.
domain assumption Arithmetic circuits can be faithfully represented as systems of polynomials over which linear and nonlinear rewriting rules are sound and complete
Core modeling assumption for algebraic circuit verification.

pith-pipeline@v0.9.0 · 5392 in / 1247 out tokens · 55583 ms · 2026-05-15T13:44:56.021647+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages

[1]

Journal of Sym- bolic Computation 35(4), 403–419 (2003)

Arnold, E.A.: Modular algorithms for computing Gröbner bases. Journal of Sym- bolic Computation 35(4), 403–419 (2003)

work page 2003
[2]

http://www.eecs.berkeley.edu/~alanmi/abc/ (2019), bitbucket Version 1.01

Berkeley Logic Synthesis and Veriﬁcation Group: ABC: A System for Sequen- tial Synthesis and Veriﬁcation. http://www.eecs.berkeley.edu/~alanmi/abc/ (2019), bitbucket Version 1.01

work page 2019
[3]

In: Proc

Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Proc. of the 36th International Conference on Computer Aided Veriﬁcation (CA V) 2024, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 133–152. Springer (2024). https://doi.org/10.1007/978-3-031-65627-9_7

work page doi:10.1007/978-3-031-65627-9_7 2024
[4]

Journal of the ACM 18(4), 478–504 (1971)

Brown, W.S.: On Euclid’s algorithm and the computation of polynomial greatest common divisors. Journal of the ACM 18(4), 478–504 (1971)

work page 1971
[5]

Buchberger, B.: Ein Algorithmus zum Auﬃnden der Basiselemente des Restk- lassenringes nach einem nulldimensionalen Polynomideal. Ph.D. thesis, University of Innsbruck (1965)

work page 1965
[6]

Under- graduate texts in mathematics, Springer, 2nd edn

Cox, D.A., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms – an Intro- duction to Computational Algebraic Geometry and Commutative Algebra. Under- graduate texts in mathematics, Springer, 2nd edn. (1997)

work page 1997
[7]

Springer (2005)

Cox, D.A., Little, J., O’Shea, D.: Using Algebraic Geometry. Springer (2005)

work page 2005
[8]

Cambridge University Press, 3rd edn

Gerhard, J., Von zur Gathen, J.: Modern Computer Algebra. Cambridge University Press, 3rd edn. (2013)

work page 2013
[9]

GMP: The GNU Multiple Precision Arithmetic Library, https://gmplib.org

work page
[10]

In: Proc

Golia, P., Soos, M., Chakraborty, S., Meel, K.S.: Designing Samplers is Easy: The Boon of Testers. In: Proc. of 2021 Formal Methods in Computer Aided Design (FMCAD). pp. 222–230 (2021). https://doi.org/10.34727/2021/isbn. 978-3-85448-046-4_31

work page doi:10.34727/2021/isbn 2021
[11]

In: Proc

Heisinger, M., Hofstadler, C.: f4ncgb: High Performance Gröbner Basis Compu- tations in Free Algebras. In: Proc. of the International Workshop on Computer Algebra in Scientiﬁc Computing (CASC) 2025. pp. 79–97. Springer (2025)

work page 2025
[12]

https://doi.org/10.4230/artifacts

Hofstadler, C., Kaufmann, D.: TalisMan. https://doi.org/10.4230/artifacts. 23376, https://github.com/d-kfmnn/talisman/tree/be8187d, software, version 1.0., swhId: swh:1:dir:8af022a61661d2b7fb281abbdc2f18d51f221c20 (visited on 2025-08-08)

work page doi:10.4230/artifacts 2025
[13]

In: Proc

Hofstadler, C., Kaufmann, D.: Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Veriﬁcation. In: Proc. of the 31st International Conference on Principles and Practice of Constraint Programming (CP) 2025. Leibniz International Proceedings in Informatics (LIPIcs), vol. 340, pp. 14:1–14:22 (2025). https://doi.org/10.4230/LIPIcs.CP.2025.14

work page doi:10.4230/lipics.cp.2025.14 2025
[14]

https://doi

Hofstadler, C., Kaufmann, D., Chen, C.: TalisMan2.0 - Artifact. https://doi. org/10.5281/zenodo.20019348 (2026) Multimodular Circuit Veriﬁcation 17

work page doi:10.5281/zenodo.20019348 2026
[15]

Journal of Symbolic Computation 137, 102581 (2026)

Hofstadler, C., Levandovskyy, V.: Modular algorithms for computing Gröbner bases in free algebras. Journal of Symbolic Computation 137, 102581 (2026)

work page 2026
[16]

Journal of Symbolic Computation 125, 102325 (2024)

Hofstadler, C., Verron, T.: Short proofs of ideal membership. Journal of Symbolic Computation 125, 102325 (2024)

work page 2024
[17]

IEICE Trans

Homma, N., Watanabe, Y., Aoki, T., Higuchi, T.: Formal design of arithmetic circuits based on arithmetic description language. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. 89-A(12), 3500–3509 (2006). https://doi.org/10.1093/ ietfec/e89-a.12.3500

work page 2006
[18]

Tahoori, and Jörg Henkel

Kaufmann, D., Beame, P., Biere, A., Nordström, J.: Adding Dual Variables to Al- gebraic Reasoning for Gate-Level Multiplier Veriﬁcation. In: Proc. of 2022 Design, Automation & Test in Europe Conf. & Exhibition (DATE). pp. 1431–1436. IEEE (2022). https://doi.org/10.23919/DATE54114.2022.9774587

work page doi:10.23919/date54114.2022.9774587 2022
[19]

In: Proc

Kaufmann, D., Berthomieu, J.: Extracting Linear Relations from Gröbner Bases for Formal Veriﬁcation of And-Inverter Graphs. In: Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). vol. 15696, pp. 355–374. Springer (2025). https://doi.org/10.1007/978-3-031-90643-5_19

work page doi:10.1007/978-3-031-90643-5_19 2025
[20]

In: Proc

Kaufmann, D., Biere, A.: AMulet 2.0 for Verifying Multiplier Circuits. In: Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 12652, pp. 357–364. Springer (2021). https://doi.org/10.1007/ 978-3-030-72013-1_19

work page 2021
[21]

Fedyukovich, S

Kaufmann, D., Biere, A., Kauers, M.: Verifying Large Multipliers by Combining SAT and Computer Algebra. In: Proc. of Formal Methods in Computer Aided Design (FMCAD). pp. 28–36. IEEE (2019). https://doi.org/10.23919/FMCAD. 2019.8894250

work page doi:10.23919/fmcad 2019
[22]

Formal Methods Syst

Kaufmann, D., Biere, A., Kauers, M.: Incremental column-wise veriﬁcation of arith- metic circuits using computer algebra. Formal Methods Syst. Des. 56(1), 22–54 (2020). https://doi.org/10.1007/s10703-018-00329-2

work page doi:10.1007/s10703-018-00329-2 2020
[23]

For- mal Methods in System Design 64(1), 73–107 (2024)

Kaufmann, D., Fleury, M., Biere, A., Kauers, M.: Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker. For- mal Methods in System Design 64(1), 73–107 (2024). https://doi.org/10.1007/ s10703-022-00391-x

work page 2024
[24]

In: Proc

Kaufmann, D., Hofstadler, C.: Recycling Algebraic Proof Certiﬁcates. In: Proc. of the 10th International Workshop on Satisﬁability Checking and Symbolic Com- putation (SC-Square) 2025. vol. 4116, pp. 35–40. Ceur (2025), https://ceur-ws. org/Vol-4116/

work page 2025
[25]

In: Irfan, A., Kaufmann, D

Konrad, A., Scholl, C.: FastPoly: An Eﬃcient Polynomial Package for the Veriﬁ- cation of Integer Arithmetic Circuits. In: Proc. of Formal Methods in Computer Aided Design (FMCAD). pp. 139–144 (2025). https://doi.org/10.34727/2025/ isbn.978-3-85448-084-6_20

work page doi:10.34727/2025/ 2025
[26]

In: Proc

Konrad, A., Scholl, C.: Symbolic Computer Algebra for Multipliers Revisited - It’s All About Orders and Phases. In: Proc. of Formal Methods in Computer-Aided Design (FMCAD). pp. 261–271. IEEE (2024). https://doi.org/10.34727/2024/ isbn.978-3-85448-065-5_32

work page doi:10.34727/2024/ 2024
[27]

In: Proc

Konrad, A., Scholl, C., Mahzoon, A., Große, D., Drechsler, R.: Divider Veriﬁca- tion Using Symbolic Computer Algebra and Delayed Don’t Care Optimization. In: Proc. of Formal Methods in Computer-Aided Design (FMCAD). pp. 1–10. IEEE (2022). https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_17

work page doi:10.34727/2022/isbn.978-3-85448-053-2_17 2022
[28]

IEEE Trans

Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property veriﬁcation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21(12), 1377–1394 (2002). https://doi.org/10. 1109/TCAD.2002.804386 18 C. Hofstadler et al

work page arXiv 2002
[29]

In: Proc

Mahzoon, A., Große, D., Drechsler, R.: Polycleaner: clean your polynomials be- fore backward rewriting to verify million-gate multipliers. In: Proc. of Intl. Conf. on Computer-Aided Design (ICCAD). ACM (2018). https://doi.org/10.1145/ 3240765.3240837

work page arXiv 2018
[30]

Ternary Compute -Enabled Memory using Ferroelectric Transistors for Accelerating Deep Neural Networks,

Mahzoon, A., Große, D., Scholl, C., Drechsler, R.: Towards Formal Veriﬁcation of Optimized and Industrial Multipliers. In: Proc. of Design, Automation & Test in Europe Conf. & Exhibition (DATE). pp. 544–549. IEEE (2020). https://doi. org/10.23919/DATE48585.2020.9116485

work page doi:10.23919/date48585.2020.9116485 2020
[31]

Advances in mathematics 46(3), 305–329 (1982)

Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in mathematics 46(3), 305–329 (1982)

work page 1982
[32]

In: Proc

Monagan, M., Pearce, R.: A compact parallel implementation of F4. In: Proc. of the 2015 International Workshop on Parallel Symbolic Computation. pp. 95–100 (2015)

work page 2015
[33]

In: Proc

Philipp, T., Steinke, P.: PBLib - A Library for Encoding Pseudo-Boolean Con- straints into CNF. In: Proc. of 18th Intl. Conf. on Theory and Applications of Satisﬁability Testing (SAT) 2015. LNCS, vol. 9340, pp. 9–16. Springer (2015). https://doi.org/10.1007/978-3-319-24318-4_2

work page doi:10.1007/978-3-319-24318-4_2 2015
[34]

Pearson Education London (2011)

Rosen, K.H.: Elementary Number Theory and Its Applications. Pearson Education London (2011)

work page 2011
[35]

Stein, W.A.: Modular Forms: A Computational Approach, vol. 79. American Math- ematical Soc. (2007)

work page 2007
[36]

The FLINT team: FLINT: Fast Library for Number Theory (2025), version 3.4.0, https://flintlib.org Multimodular Circuit Veriﬁcation 19 A Benchmark Details The components of the aoki-benchmarks are: – PPG: simple (sp), Booth encoding radix-4 (bp); – PPA: Array (ar), Wallace tree (wt), Balanced delay tree (bd), Overturned- stairs tree (os), Dadda tree (dt), ...

work page 2025

[1] [1]

Journal of Sym- bolic Computation 35(4), 403–419 (2003)

Arnold, E.A.: Modular algorithms for computing Gröbner bases. Journal of Sym- bolic Computation 35(4), 403–419 (2003)

work page 2003

[2] [2]

http://www.eecs.berkeley.edu/~alanmi/abc/ (2019), bitbucket Version 1.01

Berkeley Logic Synthesis and Veriﬁcation Group: ABC: A System for Sequen- tial Synthesis and Veriﬁcation. http://www.eecs.berkeley.edu/~alanmi/abc/ (2019), bitbucket Version 1.01

work page 2019

[3] [3]

In: Proc

Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Proc. of the 36th International Conference on Computer Aided Veriﬁcation (CA V) 2024, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 133–152. Springer (2024). https://doi.org/10.1007/978-3-031-65627-9_7

work page doi:10.1007/978-3-031-65627-9_7 2024

[4] [4]

Journal of the ACM 18(4), 478–504 (1971)

Brown, W.S.: On Euclid’s algorithm and the computation of polynomial greatest common divisors. Journal of the ACM 18(4), 478–504 (1971)

work page 1971

[5] [5]

Buchberger, B.: Ein Algorithmus zum Auﬃnden der Basiselemente des Restk- lassenringes nach einem nulldimensionalen Polynomideal. Ph.D. thesis, University of Innsbruck (1965)

work page 1965

[6] [6]

Under- graduate texts in mathematics, Springer, 2nd edn

Cox, D.A., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms – an Intro- duction to Computational Algebraic Geometry and Commutative Algebra. Under- graduate texts in mathematics, Springer, 2nd edn. (1997)

work page 1997

[7] [7]

Springer (2005)

Cox, D.A., Little, J., O’Shea, D.: Using Algebraic Geometry. Springer (2005)

work page 2005

[8] [8]

Cambridge University Press, 3rd edn

Gerhard, J., Von zur Gathen, J.: Modern Computer Algebra. Cambridge University Press, 3rd edn. (2013)

work page 2013

[9] [9]

GMP: The GNU Multiple Precision Arithmetic Library, https://gmplib.org

work page

[10] [10]

In: Proc

Golia, P., Soos, M., Chakraborty, S., Meel, K.S.: Designing Samplers is Easy: The Boon of Testers. In: Proc. of 2021 Formal Methods in Computer Aided Design (FMCAD). pp. 222–230 (2021). https://doi.org/10.34727/2021/isbn. 978-3-85448-046-4_31

work page doi:10.34727/2021/isbn 2021

[11] [11]

In: Proc

Heisinger, M., Hofstadler, C.: f4ncgb: High Performance Gröbner Basis Compu- tations in Free Algebras. In: Proc. of the International Workshop on Computer Algebra in Scientiﬁc Computing (CASC) 2025. pp. 79–97. Springer (2025)

work page 2025

[12] [12]

https://doi.org/10.4230/artifacts

Hofstadler, C., Kaufmann, D.: TalisMan. https://doi.org/10.4230/artifacts. 23376, https://github.com/d-kfmnn/talisman/tree/be8187d, software, version 1.0., swhId: swh:1:dir:8af022a61661d2b7fb281abbdc2f18d51f221c20 (visited on 2025-08-08)

work page doi:10.4230/artifacts 2025

[13] [13]

In: Proc

Hofstadler, C., Kaufmann, D.: Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Veriﬁcation. In: Proc. of the 31st International Conference on Principles and Practice of Constraint Programming (CP) 2025. Leibniz International Proceedings in Informatics (LIPIcs), vol. 340, pp. 14:1–14:22 (2025). https://doi.org/10.4230/LIPIcs.CP.2025.14

work page doi:10.4230/lipics.cp.2025.14 2025

[14] [14]

https://doi

Hofstadler, C., Kaufmann, D., Chen, C.: TalisMan2.0 - Artifact. https://doi. org/10.5281/zenodo.20019348 (2026) Multimodular Circuit Veriﬁcation 17

work page doi:10.5281/zenodo.20019348 2026

[15] [15]

Journal of Symbolic Computation 137, 102581 (2026)

Hofstadler, C., Levandovskyy, V.: Modular algorithms for computing Gröbner bases in free algebras. Journal of Symbolic Computation 137, 102581 (2026)

work page 2026

[16] [16]

Journal of Symbolic Computation 125, 102325 (2024)

Hofstadler, C., Verron, T.: Short proofs of ideal membership. Journal of Symbolic Computation 125, 102325 (2024)

work page 2024

[17] [17]

IEICE Trans

Homma, N., Watanabe, Y., Aoki, T., Higuchi, T.: Formal design of arithmetic circuits based on arithmetic description language. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. 89-A(12), 3500–3509 (2006). https://doi.org/10.1093/ ietfec/e89-a.12.3500

work page 2006

[18] [18]

Tahoori, and Jörg Henkel

Kaufmann, D., Beame, P., Biere, A., Nordström, J.: Adding Dual Variables to Al- gebraic Reasoning for Gate-Level Multiplier Veriﬁcation. In: Proc. of 2022 Design, Automation & Test in Europe Conf. & Exhibition (DATE). pp. 1431–1436. IEEE (2022). https://doi.org/10.23919/DATE54114.2022.9774587

work page doi:10.23919/date54114.2022.9774587 2022

[19] [19]

In: Proc

Kaufmann, D., Berthomieu, J.: Extracting Linear Relations from Gröbner Bases for Formal Veriﬁcation of And-Inverter Graphs. In: Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). vol. 15696, pp. 355–374. Springer (2025). https://doi.org/10.1007/978-3-031-90643-5_19

work page doi:10.1007/978-3-031-90643-5_19 2025

[20] [20]

In: Proc

Kaufmann, D., Biere, A.: AMulet 2.0 for Verifying Multiplier Circuits. In: Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 12652, pp. 357–364. Springer (2021). https://doi.org/10.1007/ 978-3-030-72013-1_19

work page 2021

[21] [21]

Fedyukovich, S

Kaufmann, D., Biere, A., Kauers, M.: Verifying Large Multipliers by Combining SAT and Computer Algebra. In: Proc. of Formal Methods in Computer Aided Design (FMCAD). pp. 28–36. IEEE (2019). https://doi.org/10.23919/FMCAD. 2019.8894250

work page doi:10.23919/fmcad 2019

[22] [22]

Formal Methods Syst

Kaufmann, D., Biere, A., Kauers, M.: Incremental column-wise veriﬁcation of arith- metic circuits using computer algebra. Formal Methods Syst. Des. 56(1), 22–54 (2020). https://doi.org/10.1007/s10703-018-00329-2

work page doi:10.1007/s10703-018-00329-2 2020

[23] [23]

For- mal Methods in System Design 64(1), 73–107 (2024)

Kaufmann, D., Fleury, M., Biere, A., Kauers, M.: Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker. For- mal Methods in System Design 64(1), 73–107 (2024). https://doi.org/10.1007/ s10703-022-00391-x

work page 2024

[24] [24]

In: Proc

Kaufmann, D., Hofstadler, C.: Recycling Algebraic Proof Certiﬁcates. In: Proc. of the 10th International Workshop on Satisﬁability Checking and Symbolic Com- putation (SC-Square) 2025. vol. 4116, pp. 35–40. Ceur (2025), https://ceur-ws. org/Vol-4116/

work page 2025

[25] [25]

In: Irfan, A., Kaufmann, D

Konrad, A., Scholl, C.: FastPoly: An Eﬃcient Polynomial Package for the Veriﬁ- cation of Integer Arithmetic Circuits. In: Proc. of Formal Methods in Computer Aided Design (FMCAD). pp. 139–144 (2025). https://doi.org/10.34727/2025/ isbn.978-3-85448-084-6_20

work page doi:10.34727/2025/ 2025

[26] [26]

In: Proc

Konrad, A., Scholl, C.: Symbolic Computer Algebra for Multipliers Revisited - It’s All About Orders and Phases. In: Proc. of Formal Methods in Computer-Aided Design (FMCAD). pp. 261–271. IEEE (2024). https://doi.org/10.34727/2024/ isbn.978-3-85448-065-5_32

work page doi:10.34727/2024/ 2024

[27] [27]

In: Proc

Konrad, A., Scholl, C., Mahzoon, A., Große, D., Drechsler, R.: Divider Veriﬁca- tion Using Symbolic Computer Algebra and Delayed Don’t Care Optimization. In: Proc. of Formal Methods in Computer-Aided Design (FMCAD). pp. 1–10. IEEE (2022). https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_17

work page doi:10.34727/2022/isbn.978-3-85448-053-2_17 2022

[28] [28]

IEEE Trans

Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property veriﬁcation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21(12), 1377–1394 (2002). https://doi.org/10. 1109/TCAD.2002.804386 18 C. Hofstadler et al

work page arXiv 2002

[29] [29]

In: Proc

Mahzoon, A., Große, D., Drechsler, R.: Polycleaner: clean your polynomials be- fore backward rewriting to verify million-gate multipliers. In: Proc. of Intl. Conf. on Computer-Aided Design (ICCAD). ACM (2018). https://doi.org/10.1145/ 3240765.3240837

work page arXiv 2018

[30] [30]

Ternary Compute -Enabled Memory using Ferroelectric Transistors for Accelerating Deep Neural Networks,

Mahzoon, A., Große, D., Scholl, C., Drechsler, R.: Towards Formal Veriﬁcation of Optimized and Industrial Multipliers. In: Proc. of Design, Automation & Test in Europe Conf. & Exhibition (DATE). pp. 544–549. IEEE (2020). https://doi. org/10.23919/DATE48585.2020.9116485

work page doi:10.23919/date48585.2020.9116485 2020

[31] [31]

Advances in mathematics 46(3), 305–329 (1982)

Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in mathematics 46(3), 305–329 (1982)

work page 1982

[32] [32]

In: Proc

Monagan, M., Pearce, R.: A compact parallel implementation of F4. In: Proc. of the 2015 International Workshop on Parallel Symbolic Computation. pp. 95–100 (2015)

work page 2015

[33] [33]

In: Proc

Philipp, T., Steinke, P.: PBLib - A Library for Encoding Pseudo-Boolean Con- straints into CNF. In: Proc. of 18th Intl. Conf. on Theory and Applications of Satisﬁability Testing (SAT) 2015. LNCS, vol. 9340, pp. 9–16. Springer (2015). https://doi.org/10.1007/978-3-319-24318-4_2

work page doi:10.1007/978-3-319-24318-4_2 2015

[34] [34]

Pearson Education London (2011)

Rosen, K.H.: Elementary Number Theory and Its Applications. Pearson Education London (2011)

work page 2011

[35] [35]

Stein, W.A.: Modular Forms: A Computational Approach, vol. 79. American Math- ematical Soc. (2007)

work page 2007

[36] [36]

The FLINT team: FLINT: Fast Library for Number Theory (2025), version 3.4.0, https://flintlib.org Multimodular Circuit Veriﬁcation 19 A Benchmark Details The components of the aoki-benchmarks are: – PPG: simple (sp), Booth encoding radix-4 (bp); – PPA: Array (ar), Wallace tree (wt), Balanced delay tree (bd), Overturned- stairs tree (os), Dadda tree (dt), ...

work page 2025