Pith. sign in

REVIEW 3 major objections 4 minor 33 references

Extracting Linear Relations from Gr\"obner Bases for Formal Verification of And-Inverter Graphs

T0 review · 3 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read For a linearized specification, a degree-ordered Gröbner basis needs only its linear polynomials to decide correctness of an and-inverter graph.

desk verdict Sound theorem, but the practical completeness claim is false. read the letter →

arxiv 2411.16348 v2 pith:HXIAZCYZ submitted 2024-11-25 cs.SC cs.LO

Daniela Kaufmann , Jérémy Berthomieu This is my paper · ORCID
classification cs.SCcs.LO MSC 13P1068W30
keywords AlgebraicReasoningGröbnerBasisHardwareVerificationAnd-InverterGraphsMultiplierDegreeReverseLexicographicOrderLinearPolynomialsIdealMembership
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper tries to establish that, once a circuit's specification is made linear, verifying an and-inverter graph can be done solely by taking constant-coefficient combinations of the linear polynomials inside a degree-first Gröbner basis; every higher-degree basis element can be ignored. The point is to sidestep the monomial blow-up that comes from rewriting a specification against a lexicographic basis. The authors prove the soundness and completeness of this reduction as Theorem 1, then turn it into a practical algorithm by computing small Gröbner bases on local sub-circuits and extracting one linear relation at a time. Their implementation verifies all tested optimized 32-, 64-, and 128-bit multiplier benchmarks and solves instances that a leading comparison tool misses, so the method appears to complement existing algebraic verification approaches.

What carries the argument

The load-bearing object is the set $G_1$ of linear polynomials inside a degree reverse lexicographic Gröbner basis, where monomials are ordered by total degree first and ties are broken from the right. Under this order, the leading monomial of any linear polynomial has degree one and its tail also has degree at most one, so reducing a linear polynomial by $G$ stays inside degree one and can only use $G_1$. The companion mechanism is linearization: fresh variables $t_i$ stand for non-linear monomials $\sigma_i$ of the specification, with extension polynomials $t_i - \sigma_i$ added to the gate polynomials, so the membership test becomes a linear one. Finally, the local-extraction loop replaces the infeasible full basis computation with repeated small drl computations on sub-circuits defined by the gate whose leading term is currently needed.

What would settle it

Run the local extraction loop on a known-correct AIG, letting the fragment grow until it contains every gate upstream of the target gate; if at that point no linear polynomial with the needed leading term has appeared, while the full degree-first Gröbner basis of the same circuit does contain one, the practical completeness claim is false. Constructing such an instance, for example a correct multiplier where a linear relation depends on a distant part of the circuit, would settle the question directly.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: if $p \in K[X]$ is linear, $I$ is an ideal, $G$ is a Gröbner basis of $I$ for the degree reverse lexicographic order $\prec_{\mathrm{drl}}$, and $G_1 = \{g \in G \mid \deg(g) \le 1\}$, then $p \in I$ if and only if $p \to_{G_1} 0$, and in that case $p$ is a $K$-linear combination of polynomials in $G_1$. The proof observes that reducing a linear polynomial by a drl-ordered basis never needs to touch a leading monomial of degree above one, so all nonlinear basis elements are irrelevant to the membership test. Because a real specification is usually nonlinear, the paper first linearizes it by replacing each non-linear monomial $\sigma_i$ with a fresh extension variable $t_i$ and adding the polynomial $t_i - \sigma_i$ (Lemma 3). The practical algorithm then avoids computing the full drl basis: for each needed leading term $v$, it builds a small sub-circuit around the gate $v$ — its children up to a growing distance, its siblings, and collected parents — computes a drl Gröbner basis for that fragment, and extracts a linear polynomial with leading term $v$. If no such polynomial appears as the fragment grows, the circuit is declared incorrect.

Load-bearing premise

The practical algorithm assumes that the small circuit fragment built around each gate is large enough to witness any linear polynomial implied by the whole circuit; if that local-to-global step fails, a correct circuit could be reported as incorrect.

Editorial extensions

If this is right

  • With the theorem, a linearized specification can be verified by linear algebra alone: no intermediate reduction result ever exceeds degree one, so monomial blow-up in the specification rewrite disappears.
  • Only the linear tail of the drl Gröbner basis needs to be kept for the final membership decision; nonlinear elements matter only insofar as they help generate those linear polynomials.
  • The local-extraction strategy makes this usable on optimized, synthesis-scripted multipliers, where structure-dependent tools time out because the classical component boundaries are blurred.
  • The approach complements existing verifiers: it solves instances with carry-lookahead adder chains that cause blow-up in other algebraic tools, while remaining competitive on standard ABC benchmarks.
  • For an incorrect circuit, failure to find a linear polynomial with the required leading term, once the local fragment covers all topologically smaller gates, certifies that the specification is not implied.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The proof of Theorem 1 generalizes to any fixed-degree specification: if $\deg(p)=d$, reduction under drl only ever consults basis elements of degree at most $d$, so the analogous restricted set $G_{\le d}$ would decide membership; the paper only states the linear case, but the same argument carries through.
  • The practical completeness claim rests on a local-to-global sufficiency that the paper asserts rather than proves: the fragment $C_{v,d}$ must witness every linear relation the full ideal implies, so a fallback that escalates to a larger region when local extraction saturates without finding the relation would make the tool's 'incorrect' answer safer.
  • Since the linear relations produced are cheap, they could be fed back into the lexicographic encoding as rewrite rules, effectively combining the degree-based extraction with the substitution-style reduction used in earlier algebraic verifiers.
  • The technique should transfer to other acyclic arithmetic circuits whose specifications become linear after extension variables, including adders and datapath components, whenever the local fragment assumption holds.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes an algebraic verification method for and-inverter graphs (AIGs) based on extracting linear polynomials from degree reverse lexicographic (drl) Gröbner bases. The theoretical part proves Theorem 1: for a drl-Gröbner basis G of an ideal I, a linear polynomial p lies in I if and only if p reduces to zero using only the degree-≤1 polynomials G1 of G. The paper also proves Lemma 3 on linearizing a specification by introducing extension variables. To avoid computing a full drl-Gröbner basis for large circuits, the paper presents Algorithms 2–4, which compute drl-Gröbner bases for local sub-circuits and extract a linear polynomial with a desired leading term; the paper claims that failure to find such a polynomial implies the circuit is incorrect, citing Theorem 1. The method is implemented in the tool MultiLinG and evaluated on multiplier benchmarks, including optimized ABC multipliers and aoki multipliers.

Significance. Theorem 1 and Lemma 3 are elegant and correctly proved; they show that for a complete drl-Gröbner basis the ideal membership of a linear specification can be decided using only linear operations, avoiding monomial blow-up in the reduction phase. The paper makes the theoretical contribution accessible and demonstrates a working implementation on real multiplier benchmarks, including optimized circuits that are hard for previous algebraic tools. However, the practical completeness claim—that the local sub-circuit computation in Algorithm 4 is sufficient to witness all linear relations present in the full ideal—is not justified and is in fact false. The provided counterexample shows that Algorithm 2 can return a 'circuit incorrect' verdict for a correct circuit, so the method as described is not a sound decision procedure for AIG verification. The theoretical result remains valuable, but the practical algorithm needs either a correctness proof under explicit sufficient conditions or a repositioning as a heuristic.

major comments (3)
  1. [Section 4.2] The sentence 'If we still did not find a linear polynomial at this point, we know that the circuit is incorrect. This follows from Theorem 1' is not a valid inference. Theorem 1 applies to a drl-Gröbner basis of the entire ideal I of the full circuit. Algorithm 4 computes a drl-Gröbner basis only for the ideal generated by the gate polynomials of a local sub-circuit C_{v,d}. The absence of a linear polynomial with leading term v in that local ideal does not imply its absence in I. A concrete counterexample is an AIG with inputs a,b,c,d and gates x=a∧b, y=c∧d, v=x∧y, p=a∧c, q=b∧d, u=p∧q. In the Boolean ring, v=u=abcd, so v−u is in the full circuit ideal I. For a variable order with v>u, the reduced drl-Gröbner basis of I contains a linear polynomial with leading term v. Yet the sub-circuit C_v constructed by Algorithm 4 includes v, x, y, a, b, c, d and their parents, but never u, because u is neither an ancestor nor a sibling of v. The ideal generated by the local gate polynomials contains no linear polynomial with leading term v, since v occurs only in the quadratic polynomial v−xy. Algorithm 4 therefore returns ∅ and Algorithm 2 returns ⊥ for a circuit that is correct, so the claimed completeness, and even the soundness of the ⊥ verdict, is false. The authors must either prove a local completeness theorem with explicit sufficient conditions on the sub-circuit, or weaken the claim so that a failed local extraction yields 'unknown' rather than 'incorrect'.
  2. [Algorithm 4 (Section 4.2)] The construction of C_{v,d}—including v, its children up to distance d, siblings, and parents of the collected nodes—does not, even as d reaches dist(v), cover all gates that are topologically smaller than v in the whole DAG. The statement in the text that in the worst case the algorithm has computed a full drl-Gröbner basis 'for all gate polynomials that are topologically smaller than v' is inaccurate: only ancestors of v (plus their siblings and parents) are collected, not arbitrary gates that appear earlier in the topological order, such as independent implementations u in the counterexample above. A completeness proof for Algorithm 4 would need to show that any linear polynomial with leading term v in the full ideal is contained in the ideal generated by the polynomials of the constructed sub-circuit; the counterexample shows this is not true in general, so the proof obligation is substantial and cannot be discharged by invoking Theorem 1.
  3. [Section 5.1, Section 5.3] The experimental evaluation does not report cases where the tool fails despite the circuit being correct, i.e., where local extraction misses a linear relation. On the aoki benchmarks MultiLinG solves only 29 of 192 instances, but the paper attributes the failures to time/memory limits and does not analyze whether any of the 163 unsolved instances would be rejected if allowed more resources. Given the false-negative counterexample in Section 4.2, the paper should measure and report the rate of wrong 'incorrect' verdicts on correct circuits, or adjust the algorithm to return 'unknown' when the full drl-Gröbner basis is not computed. Without such data or a correctness guarantee, the presented method cannot be regarded as a formal verification technique, and the empirical claims need to be qualified accordingly.
minor comments (4)
  1. [Section 3, proof of Theorem 1] The phrase 'the division algorithm ... will only select polynomials in G whose leading monomials also have degree 1' is slightly imprecise: a reduction step selects a polynomial whose leading monomial divides the current leading monomial, and for a linear polynomial only degree-1 leading monomials can divide it. Rephrasing this would improve clarity.
  2. [Section 4.2, Algorithm 4] The initial distance d=3 and the depth-dependent fall-back to non-linear rewriting for distances below six are heuristic parameters that are not part of the completeness argument. The paper should explicitly state that these choices are heuristics and do not affect the theoretical guarantees only if the local-completeness claim is abandoned or proven under different hypotheses.
  3. [Section 5.1] The fall-back to non-linear rewriting when the distance of a node to the primary inputs is below six is a further heuristic whose interaction with the claimed completeness is not discussed. If this fall-back is used, the reduction is no longer performed only by linear polynomials, so even the conditional completeness obtained from a full drl-Gröbner basis would not apply to the resulting reduction path.
  4. [Section 2.2, Definition 10] The four gate-polynomial forms are all of degree two, but the observation that the polynomial encoding forms a Gröbner basis with respect to the lexicographic order relies on the UMLT property and on the Boolean input polynomials; citing the precise result (e.g., the relevant theorem from the authors' earlier work) at this point would help the reader.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: Theorem 1 and Lemma 3 are proved from standard Gröbner-basis facts; the §4.2 local-completeness statement is a correctness gap, not a self-referential derivation.

full rationale

The paper's central theoretical claim, Theorem 1, is not circular. Its proof uses only the standard unique-remainder property of Gröbner bases together with the observation that a degree-1 polynomial being reduced under ≼drl can only have its leading monomial cancelled by polynomials in G1 whose leading monomials have degree 1; no assumption equivalent to the conclusion is imported. Lemma 3's linearization step is likewise proved in both directions: extension variables are introduced as new indeterminates, and ideal membership of p is shown equivalent to membership of the linearized polynomial in the extended ideal, which is a genuine equational equivalence rather than a fitted input. Algorithm 1's correctness is then a direct consequence of Theorem 1. The later local Algorithm 4 contains the sentence 'If we still did not find a linear polynomial at this point, we know that the circuit is incorrect. This follows from Theorem 1.' That statement is not circular, but it is an invalid transfer of a global Gröbner-basis property to a sub-circuit ideal, so it is a soundness/completeness concern rather than a self-referential derivation. References to the authors' earlier AMulet2 arithmetic and to [19] for local rewriting are implementation reuse and an independently stated theorem; they do not carry the proof of the new result. There is no load-bearing self-citation, no fitted parameter renamed as a prediction, and no definition that presupposes the target result.

Assumptions & free parameters 2 free parameters · 4 assumptions · 1 invented entities

The central mathematical claim is parameter-free and rests on standard Gröbner basis theory plus two domain assumptions about acyclic Boolean circuits. The practical method introduces two hand-tuned thresholds and one unproven local sufficiency assumption, which is the main source of correctness risk. Extension variables are auxiliary and fully defined.

free parameters (2)
  • initial local basis depth d = 3
    Algorithm 4 starts with d=3 because preprocessing already produces most linear polynomials at d=2; this threshold is hand-tuned for benchmark performance.
  • non-linear fallback distance threshold = 6
    Section 5.1: nodes with distance below 6 fall back to non-linear rewriting if linearization fails, chosen empirically to handle Booth encodings; this changes the algorithm's behavior and affects the purity of the linear approach.
assumptions (4)
  • standard math Standard Gröbner basis theory: existence, uniqueness of remainder, and the division algorithm (Lemmas 1-2 from Cox et al.).
    Used throughout Section 3 to argue that p in I if and only if p reduces to 0 with respect to a Gröbner basis.
  • domain assumption The AIG is acyclic, so a total term order exists where each gate's output variable is greater than its inputs.
    Section 3 states that cycles would prevent a canonical total order and a Gröbner basis; this is the precondition for the polynomial encoding.
  • domain assumption Primary inputs are Boolean, encoded by a_i^2 - a_i, and the polynomial arithmetic engine reduces exponents x*x = x.
    Section 5.1: the tool inherits AMulet2's Boolean polynomial arithmetic, which is required for the ideal membership semantics of the circuit.
  • ad hoc to paper The local sub-circuit C_{v,d} built in Algorithm 4 is sufficient to witness any linear polynomial of the full ideal with leading term v.
    Unproven; used in Algorithm 4 and in the completeness argument after it. Theorem 1 only applies to a full drl-Gröbner basis, not to local sub-bases.
invented entities (1)
  • extension variables t_i for non-linear monomials in the specification independent evidence
    purpose: Replace non-linear terms sigma in the specification so that the specification becomes linear and Theorem 1's linear reduction applies.
    Strictly formal auxiliary variables defined by equations t_i - sigma_i; their behavior is fully specified in Lemma 3 and they are standard linearization artifacts, not unverified physical entities.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Extracting Linear Relations from Gr\"obner Bases for Formal Verification of And-Inverter Graphs." pith.science (2026). https://pith.science/paper/HXIAZCYZ

@misc{pith2026241116348,
  author       = {Pith},
  title        = {Pith review of: Extracting Linear Relations from Gr\"obner Bases for Formal Verification of And-Inverter Graphs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HXIAZCYZ}},
  note         = {Machine review of arXiv:2411.16348}
}
read the original abstract

Formal verification techniques based on computer algebra have proven highly effective for circuit verification. The circuit, given as an and-inverter graph, is encoded as a set of polynomials that automatically generates a Gr\"obner basis with respect to a lexicographic term ordering. Correctness of the circuit can be derived by computing the polynomial remainder of the specification. However, the main obstacle is the monomial blow-up during the rewriting of the specification, which leads to the development of dedicated heuristics to overcome this issue. In this paper, we investigate an orthogonal approach and focus the computational effort on rewriting the Gr\"obner basis itself. Our goal is to ensure the basis contains linear polynomials that can be effectively used to rewrite the linearized specification. We first prove the soundness and completeness of this technique and then demonstrate its practical application. Our implementation of this method shows promising results on benchmarks related to multiplier verification.

Figures

Figures reproduced from arXiv: 2411.16348 by the authors.

Figure 1
Figure 1. AIG and polynomial encoding of a 2-bit multiplier in the ring Q[X]. Together with the specification polynomial, we fix the polynomial ring K[X] of the encoding. Although the nodes in an AIG compute logical conjunction over Boolean variables, the specification can encode richer relations. Hence, the encoding is not restricted to the Boolean ring B[X], but may include different coefficient domains, such as integers or… view at source ↗
Figure 2
Figure 2. Results of aoki-benchmarks 10 0 10 1 10 2 MultiLinG 10 0 10 1 10 2 DPOO [PITH_FULL_IMAGE:figures/full_fig_p016_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 19 canonical work pages

  1. [1]

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

    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

    work page 2019

  2. [2]

    In: ISSAC

    Berthomieu, J., Neiger, V., Safey El Din, M.: Faster Change of Order Algorithm for Gröbner Bases under Shape and Stability Assumptions. In: ISSAC. pp. 409–418. ACM (2022). https://doi.org/10.1145/3476446.3535484

    arXiv 2022

  3. [3]

    In: ISSAC

    Berthomieu, J., Eder, C., Safey El Din, M.: msolve: A Library for Solving Poly- nomial Systems. In: ISSAC. pp. 51–58. ACM (2021). https://doi.org/10.1145/ 3452143.3465545

    arXiv 2021

  4. [4]

    In: SAT Competition 2016

    Biere, A.: Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016. In: SAT Competition 2016. Dep. of Computer Science Report Series B, vol. B-2016-1, pp. 65–66. University of Helsinki (2016)

    work page 2016

  5. [5]

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

    work page 1965

  6. [6]

    Scholarpedia5(10), 7763 (2010), http: //www.scholarpedia.org/article/Groebner_basis

    Buchberger, B., Kauers, M.: Gröbner basis. Scholarpedia5(10), 7763 (2010), http: //www.scholarpedia.org/article/Groebner_basis

    work page 2010

  7. [7]

    Chen, Y., Bryant, R.E.: Verification of Arithmetic Circuits with Binary Moment Diagrams. In: DAC. pp. 535–541. ACM (1995). https://doi.org/10.1145/217474. 217583

    work page doi:10.1145/217474 1995

  8. [8]

    Springer-Verlag New York (1997)

    Cox, D., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms. Springer-Verlag New York (1997)

    work page 1997

Show all 33 references
  1. [9]

    Journal of Pure and Applied Algebra 139(1), 61–88 (1999)

    Faugère, J.Ch.: A New Efficient Algorithm for Computing Gröbner bases (F4). Journal of Pure and Applied Algebra 139(1), 61–88 (1999). https://doi.org/10. 1016/S0022-4049(99)00005-5

    1999

  2. [10]

    https://doi.org/10.1145/2608628.2608669

    Faugère, J.Ch., Gaudry, P., Huot, L., Renault, G.: Sub-Cubic Change of Ordering forGröbnerBasis:AProbabilisticApproach.In:ISSAC.pp.170–177.ACM(2014). https://doi.org/10.1145/2608628.2608669

    2014

  3. [11]

    Faugère, J.Ch., Gianni, P., Lazard, D., Mora, T.: Efficient Computation of Zero- dimensional Gröbner Bases by Change of Ordering. J. Symbolic Comput.16(4), 329–344 (1993). https://doi.org/10.1006/jsco.1993.1051

    1993

  4. [12]

    Journal of Symbolic Compu- tation 80(3), 538–569 (2017)

    Faugère, J.Ch., Mou, C.: Sparse FGLM algorithms. Journal of Symbolic Compu- tation 80(3), 538–569 (2017). https://doi.org/10.1016/j.jsc.2016.07.025

    2017 doi

  5. [13]

    IEICE Trans

    Homma, N., Watanabe, Y., Aoki, T., Higuchi, T.: Formal Design of Arithmetic Circuits Based on Arithmetic Description Language. IEICE Trans. Fundam. Elec- tron. Commun. Comput. Sci. 89-A(12), 3500–3509 (2006). https://doi.org/10. 1093/IETFEC/E89-A.12.3500

    2006

  6. [14]

    Kaufmann, D.: MultiLinG (2025), https://www.github.com/d-kfmnn/multiling

    2025

  7. [15]

    In: DATE

    Kaufmann, D., Beame, P., Biere, A., Nordström, J.: Adding dual variables to al- gebraic reasoning for gate-level multiplier verification. In: DATE. pp. 1431–1436. IEEE (2022). https://doi.org/10.23919/DATE54114.2022.9774587

    2022

  8. [16]

    https://doi.org/10.5281/zenodo.14609934

    Kaufmann, D., Berthomieu, J.: MultiLinG - Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs (Artifact) (2025). https://doi.org/10.5281/zenodo.14609934

    2025 doi

  9. [17]

    In: TACAS (2)

    Kaufmann, D., Biere, A.: Amulet 2.0 for verifying multiplier circuits. In: TACAS (2). LNCS, vol. 12652, pp. 357–364. Springer (2021). https://doi.org/10.1007/ 978-3-030-72013-1_19 Linear Gröbner Basis Polynomials for AIG Verification 19

    2021

  10. [18]

    In: FMCAD 2019

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

    2019

  11. [19]

    Formal Methods Syst

    Kaufmann, D., Biere, A., Kauers, M.: Incremental Column-wise verification of arithmetic circuits using computer algebra. Formal Methods Syst. Des.56(1), 22– 54 (2020). https://doi.org/10.1007/S10703-018-00329-2

    2020 doi

  12. [20]

    Formal Methods Syst

    Kaufmann, D., Fleury, M., Biere, A., Kauers, M.: Practical Algebraic Calcu- lus and Nullstellensatz with the Checkers Pacheck and Pastèque and Nuss- Checker. Formal Methods Syst. Des. 64(1), 73–107 (2022). https://doi.org/10. 1007/s10703-022-00391-x

    2022

  13. [21]

    In: FMCAD 2024

    Konrad, A., Scholl, C.: Symbolic Computer Algebra for Multipliers Revisited - It’s All About Orders and Phases. In: FMCAD 2024. pp. 261–271. TU Wien Academic Press (2024). https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_32

    2024 doi

  14. [22]

    Konrad, A., Scholl, C., Mahzoon, A., Große, D., Drechsler, R.: Divider verification usingsymboliccomputeralgebraanddelayeddon’tcareoptimization.In:FMCAD. pp. 1–10. IEEE (2022). https://doi.org/10.34727/2022/ISBN.978-3-85448-053-2_ 17

    2022 doi

  15. [23]

    IEEE TCAD21(12), 1377–1394 (2002)

    Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE TCAD21(12), 1377–1394 (2002). https://doi.org/10.1109/TCAD.2002.804386

    2002

  16. [24]

    IEEE TCAD pp

    Li, R., Li, L., Yu, H., Fujita, M., Jiang, W., Ha, Y.: Refscat: Formal verification of logic-optimized multipliers via automated reference multiplier generation and sca- sat synergy. IEEE TCAD pp. 1–1 (2024). https://doi.org/10.1109/TCAD.2024. 3442987

    2024 doi

  17. [25]

    In: FMCAD 2020

    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 (2020). https://doi.org/ 10.34727/2020/ISBN.978-3-85448-042-6_27

    2020 doi

  18. [26]

    In: DATE

    Liu, H., Liao, P., Huang, J., Zhen, H.L., Yuan, M., Ho, T.Y., Yu, B.: Parallel gröb- ner basis rewriting and memory optimization for efficient multiplier verification. In: DATE. pp. 1–6 (2024). https://doi.org/10.23919/DATE58400.2024.10546568

    2024

  19. [27]

    IEEE TCAD32(9), 1409–1420 (2013)

    Lv, J., Kalla, P., Enescu, F.: Efficient Gröbner Basis Reductions for Formal Verifi- cation of Galois Field Arithmetic Circuits. IEEE TCAD32(9), 1409–1420 (2013). https://doi.org/10.1109/TCAD.2013.2259540

    2013

  20. [28]

    In: ICCAD 2018

    Mahzoon,A.,Große,D.,Drechsler,R.:PolyCleaner:CleanyourPolynomialsbefore Backward Rewriting to verify Million-gate Multipliers. In: ICCAD 2018. pp. 129:1 – 129:8. ACM (2018). https://doi.org/10.1145/3240765.3240837

    2018

  21. [29]

    In: DATE

    Mahzoon, A., Große, D., Scholl, C., Drechsler, R.: Towards formal verification of optimized and industrial multipliers. In: DATE. pp. 544–549. IEEE (2020). https: //doi.org/10.23919/DATE48585.2020.9116485

    2020

  22. [30]

    Advances in Mathematics46(3), 305–329 (1982)

    Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commuta- tive semigroups and polynomial ideals. Advances in Mathematics46(3), 305–329 (1982). https://doi.org/10.1016/0001-8708(82)90048-2

    1982 doi

  23. [31]

    Journal of Complexity60, 101502 (2020)

    Neiger, V., Schost, É.: Computing syzygies in finite dimension using fast linear algebra. Journal of Complexity60, 101502 (2020). https://doi.org/10.1016/j.jco. 2020.101502

    2020

  24. [32]

    Sharangpani, H., Barton, M.L.: Statistical analysis of floating point flaw in the pentium processor (1994)

    1994

  25. [33]

    In: TACAS (1)

    Temel, M.: Vescmul: Verified implementation of s-c-rewriting for multiplier veri- fication. In: TACAS (1). LNCS, vol. 14570, pp. 340–349. Springer (2024). https: //doi.org/10.1007/978-3-031-57246-3_19 20 D. Kaufmann and J. Berthomieu A Complete Gröbner basis for two-bit multip...

    2024 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.