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

Computer algebra-based formal verification techniques have proven to be highly effective in verifying gate-level arithmetic circuits. As digital systems become more complex, ensuring the accuracy of arithmetic circuits is essential, particularly in safety-critical fields like cryptography and signal processing, where even minor errors can lead to significant consequences. Formal verification approaches on the word-level based on theorem provers [25] or computer algebra [17, 15, 18, 13], particularly those leveraging Gröbner bases [4], have demonstrated significant advancements in recent years.

These methods encode circuits given as and-inverter graphs (AIGs) [19] as polynomial systems where the coefficients are integers and the variables represent Boolean values. The terms are sorted according to a reverse topological term order [20]. This ensures that the output variable of a gate precedes its input variables, which results in an encoding where all the leading terms are disjoint. Hence, the set of gate polynomials automatically generates a Gröbner basis with respect to a lexicographic term order. This fact admits verification to be performed by simply computing the remainder of the specification polynomial modulo the Gröbner basis. The circuit is correct if and only if the final remainder is zero [16].

However, a major bottleneck of using a lexicographic term order is the significant growth of intermediate reduction results. This phenomenon, known as monomial blow-up, occurs because the tails of the polynomials in the lexicographic Gröbner basis have higher degrees than their leading terms, and can easily lead to intermediate reduction results with millions of monomials [21]. To address this challenge, various preprocessing and rewriting algorithms have been developed, which syntactically or semantically analyze the input circuit to remove redundant information and choose a suitable reduction order.

Several advanced reduction engines that use a lexicographic order have been developed, including DynPhaseOrderOpt [17], DyPoSub [22], and AMulet2 [15, 14], along with its variant TeluMA [12]. The work in [15, 14] employs SAT solving to rewrite parts of the multiplier before applying an incremental column-wise verification algorithm. A subsequent refinement in [12] eliminated the external SAT solver by using a sophisticated algebraic encoding that includes polarities of literals. In [22], a dynamic rewriting approach is used that determines the reduction order on-the-fly and backtracks if the size of the intermediate reductions exceeds a predefined threshold. Building on this, [17] introduced an improved method that incorporates mixed signals into the encoding.

Recent work [13] diverges from the lexicographic order and opts instead for a degree-compatible order to ensure that the degree of intermediate reduction results cannot increase during reduction. By first linearizing the specification polynomial, the entire reduction is restricted to linear polynomials. However, this approach requires extracting linear polynomials from the circuit, which is not straightforward. The authors proposed an on-the-fly technique that identifies subcircuits and computes degree-compatible Gröbner bases only for them. The required linear polynomials for reduction are supposed to be contained in the individually computed Gröbner bases.

Despite its innovation, the approach of [13] has notable limitations. First, it disregards that the polynomials already form a lexicographic Gröbner basis, thereby missing important structural advantages. Second, the method relies on an off-the-shelf computer algebra system (CAS), which requires explicitly encoding that all variables are Boolean, missing out on optimizations provided by modified polynomial operations. Third, whenever the initial subcircuit selection is inadequate, the subcircuit must be iteratively expanded, leading to repeated incremental Gröbner basis computations. Since CASs cannot recognize that parts of the input already generate a partial Gröbner basis, expensive computations must be repeated. Our work aims to address these shortcomings.

In this work, we introduce a novel method for extracting linear polynomials from subcircuits. Our hybrid approach combines an FGLM-based linear extraction algorithm with a guess-and-prove-style linearization technique.

In the FGLM-based algorithm, we initially compute the normal forms of single variables with respect to the lexicographic Gröbner basis. The linear polynomials are then recovered by determining the kernel of the corresponding coefficient matrix, which ensures that the linear extractions are proven to be correct. This algorithm can be considered as the first steps of the change-of-order FGLM-algorithm [8] for converting a Gröbner basis w.r.t. one term order into one for a different order. The guess-and-prove linearization approach involves sampling input values for the subcircuit. By solving a linear system of equations generated from these samples, we can identify potentially valid linear polynomials. We prove the correctness of the guessed polynomials using satisfiability (SAT) solving. To repair incorrect guesses, we exploit information obtained from the SAT solving process.

Despite taking advantage of properties that are characteristic for circuit verification, we highlight that our methods are not restricted to this application and can be used in any context that meets these characteristics. Therefore, we introduce the FGLM and guess-and-prove algorithms in a general setting in Section 3, before discussing how to specialize them for circuit verification in Section 4.

We further enhance our method by reusing computations for isomorphic subcircuits, and by generating and propagating vanishing monomials, see Section 4.1. We implement our techniques in a new tool, called TalisMan. Our experimental evaluation (Section 5) shows that we significantly outperform existing linearization techniques.

In Section 2.1, we recall basic concepts about polynomials and Gröbner bases that will be needed for the rest of this work. For further information, we refer to the great introductory books [6, 5], which also served as basis for our presentation. Section 2.2 introduces AIGs and how they can be encoded into polynomials.

A key step in our approach to circuit verification is identifying linear polynomials in a given ideal. In this section, we propose two methods that recover linear polynomials by exploiting essential properties of the ideals in our application.

We highlight that, while these techniques are designed to take advantage of these properties, they are not specific to our application and can be used in any context that meets our assumptions about the ideals involved. Formally, we consider the following problem over a (computable) field $𝕂$:

• Given: an ideal $I\subseteq 𝕂[X]$
  Compute: the set $𝕃(I)$ of all linear polynomials in $I$

Note that $𝕃(I)$ is non-empty because it always contains the zero polynomial. Moreover, if $p,q\in 𝕃(I)$, then so are $p+q$ and $cp$ for every $c\in 𝕂$. Thus, we obtain the following result.

We now discuss how we use the FGLM-style linearization and guess-and-prove-style linearization algorithms of the previous section in the context of multiplier verification.

Multipliers typically consist of three components:

1. 1.

   partial product generation (PPG), where the individual bitwise products are computed,

2. 2.

   partial product accumulation (PPA), where these products are combined using compression techniques such as Wallace trees or Dadda trees, and

3. 3.

   the final-stage adder (FSA), which produces the final multiplication result. The FSA is particularly critical in determining circuit efficiency, and may use advanced addition techniques like carry-lookahead techniques to speed up computation.

The main loop of our approach to circuit verification is outlined in Algorithm 3. The structure of this loop follows the idea from [13] of linearizing only subcircuits instead of attempting to extract linear polynomials from the entire circuit. We discuss optimizations of Algorithm 3 in Section 4.1.

Line 1 – 2: We encode the circuit using the translation presented in Definitions 8 and 9, and linearize the specification polynomial $𝒮\in 𝕂[X]$ by replacing every non-linear monomial $m_i$ by a new variable $y_i$ and adding the set $\mathrm{\Gamma }=\{y_i-m_i\mid y_i\notin X\wedge m_i\in 𝒮\wedge \mathrm{deg}(m_i)>1\}$ to the set of gate polynomials. The correctness proof for this step can be found in [13, Lem. 3].

Line 3: We apply the same basic preprocessing techniques as in [13]. That is, we eliminate all gates that only occur positively and detect vanishing monomials. Vanishing monomials are pairs of nodes that have the same children, but with different polarities. Thus, the product of the parent nodes is equal to zero. We additionally enhance the preprocessing by propagating vanishing monomials, see Section 4.1.

Furthermore, we identify and mark parts of the circuit that require dedicated reasoning. In the case of multiplier circuits, these correspond to the FSA. Whenever the FSA employs carry-lookahead techniques, we must treat the entire FSA as a single subcircuit to derive the required linear polynomials. This necessity arises because carry-lookahead techniques compute carries in parallel, unlike sequential approaches such as ripple-carry adders. For identifying these subcircuits, we utilize the cut identification method implemented in AMulet2 [15].

Line 4 – 6: The algorithm then iterates over the linearized specification as long as we have a gate polynomial in the encoding that has the same leading monomial as the linearized specification. In each iteration, we generate a subcircuit with root node $g$ for which we perform the linearization. If no matching linearized polynomial $p_{\mathrm{lin}}$ is found, we increase the subcircuit size until completion. This is the case when the subcircuit contains all gates that are topologically smaller than $g$.

Line 7: We identify the subcircuit as follows. If the root node $g$ contains a marking, i.e., if it belongs to a pattern identified in line 3, all nodes with the same marking are collected and returned. For unmarked nodes, the algorithm initially constructs a subcircuit $G_{\mathrm{sub}}$ by collecting all nodes up to a given depth $d$ with a fanout size below the specified limit $f_{\mathrm{out}}$. Our initial values are $d=2$ and $f_{\mathrm{out}}=4$ as this has empirically shown to be the most efficient. Additionally, we include all nodes whose children are already part of $G_{\mathrm{sub}}$. We also promote all input nodes of $G_{\mathrm{sub}}$ with a fanout of one to be included in $G_{\mathrm{sub}}$.

Rather than immediately increasing the depth $d$ in following iterations, we attempt to expand the subcircuit by adding individual input nodes of $G_{\mathrm{sub}}$. The expansion prioritizes the largest input node, based on our predefined variable ordering that still has a fanout size at most $f_{\mathrm{out}}$. However, every 15 iterations, the algorithm restarts with incremented depth and fanout limits. The threshold of 15 was empirically selected to keep the alternations between the depth-first and breath-first selection approaches balanced.

In that sense, our subcircuit selection algorithm is more sophisticated than the one in [13], which did not consider expanding the subcircuit by individual nodes, neither was there a limit on the fanouts nor were special markings considered.

Line 8: If $G_{\mathrm{sub}}$ is of moderate size, that is, the number of polynomials is less than 100, and the depth is at most 5 (which in our setting corresponds to all subcircuits except the marked FSA), we use the FGLM-based extraction method.

There is one exception: we also use the FGLM-based extraction method for FSA where, after preprocessing, we detect polynomials with a degree greater than the input bitwidth of the circuit, but consisting only of two terms. We detected that the guess-and-prove approach will mostly produce incorrect guesses for such polynomials due to the high-degree monomials evaluating to zero exponentially often and evaluating to 1 only for one particular input.

Line 9: For larger subcircuits with polynomials of moderate degree, we use the guess-and-prove approach to avoid excessive growth in normal forms, which would cause the computation to stall in the FGLM-style algorithm.

First of all, let us note that the ideals arising from the subcircuits satisfy all assumptions made in Section 3.2. They are zero-dimensional and radical because they contain, by definition, the Boolean value polynomials for all variables. The presence of these polynomials also takes care of the third assumption: Even if a considered ideal $I$ is formally defined over a field $𝕂$ that is not algebraically closed, we can implicitly treat it as defined over the algebraic closure $\overline{𝕂}$¹¹1 The algebraic closure $\overline{𝕂}$ of a field $𝕂$ is the smallest algebraically closed field containing $𝕂$. Every field has an algebraic closure. For instance, $\overline{ℝ}=ℂ$. of $𝕂$. The Boolean value polynomials ensure that the underlying variety $V(I)$ remains unchanged, which guarantees that our algorithm will return the correct result.

We instantiate the sample and verify plugins required in Algorithm 2 as follows. For sampling, we apply an adaptive strategy. In the first iteration, we randomly draw values 0 and 1 for all the inputs of the subcircuit and propagate the signals according to the gate structure of the subcircuit. We draw at least 10 times the size of gates in $G_{\mathrm{sub}}$ samples, but at most $\mathrm{10\hspace{0.17em}000}$. This ensures that we have enough samples, while keeping the matrix $A$ in Algorithm 2 at a computationally manageable size. To ensure that every input appears with both polarities, we also include the trivial samples by setting all inputs to 0 and to 1, respectively. If more than one iteration is required in Algorithm 2, we switch from random sampling to the repair strategy discussed at the end of Section 3.2. Using our verification plugin, we can compute witnesses for wrong guesses in the form of points in the variety and only append those witnesses to the matrix in subsequent iterations. We call our strategy adaptive-binary-sampling (AdBinSample).

As a verification technique, we use SAT solving (SAT). Verifying that a guessed polynomial $f$ lies in the ideal induced by $G_{\mathrm{sub}}$ corresponds to showing that $f$ equals zero for all signals that can pass through the circuit. To show this, we assume $f\ne 0$ and show unsatisfiability. We first encode each AIG gate that belongs to $G_{\mathrm{sub}}$ into conjunctive normal form (CNF). To translate $f\ne 0$, we split it into two pseudo-Boolean (PB) constraints and $f>0$, both of which we translate into CNF using pblib [23]. pblib does not offer a direct encoding of $\ne$. We make two SAT calls using the SAT solver Kissat [3]: one for the constraint and another for $f>0$. If $f=0$, both calls have to return “unsatisfiable”.

We acknowledge that we could also use a PB solver, such as RoundingSat [7], directly without making the detour of translating everything to CNF. We have tried this, and there was no computational difference. All instances that could be solved using Kissat could also be solved by RoundingSat in the same time. However, we decided to go with Kissat because it was easier to integrate directly into our C++ implementation.

If one instance or $f>0$ is satisfiable, we collect the satisfying assignment provided by Kissat as a witness for the wrong guess and add it as a sample in the next iteration of the guess-and-prove algorithm. This ensures that the incorrect guess $f$ cannot reappear in future iterations, leading to a faster convergence of the guessing procedure.

Moreover, by using Lemma 15, we can also quickly identify situations when the considered subcircuit was chosen too small. We are only interested in finding a linear polynomial in $G_{\mathrm{sub}}$ that involves the variable $\mathrm{lm}(g)$. If, at some point in Algorithm 2, the candidate set $L$ does not contain any polynomial involving this variable, then Lemma 15 implies that no such polynomial can exist in $G_{\mathrm{sub}}$ (even if the candidate set $L$ still contains incorrect guesses). Thus, in such a situation, we can immediately abort Algorithm 2 and extend $G_{\mathrm{sub}}$.

Line 10– 13: In case our linearization was successful, we extract $p_{\mathrm{lin}}$ from $L$ to reduce the specification. If no polynomial $p_{\mathrm{lin}}$ was found after choosing $G_{\mathrm{sub}}$ as large as possible, we return false. We reduce the linearized specification $S_{\mathrm{lin}}$ by $p_{\mathrm{lin}}$. After the main loop terminates, that is, when $S_{\mathrm{lin}}$ cannot be reduced any further, we return whether the final result is equal to zero.

We have implemented Algorithm 3 in a new C++ tool, called TalisMan. We highlight that TalisMan is not restricted to circuit verification, but it can handle any AIG.

We now evaluate TalisMan and compare it to related work [13, 14, 12, 17] using a total of 207 integer multiplier benchmarks. All benchmarks represent correct multipliers, meaning the circuits satisfy their specifications. We consider two types of benchmarks: structured circuits, where the components of a multiplier are clearly recognizable, and synthesized circuits, where gates are merged and rewritten to optimize the circuit, blurring component boundaries and complicating direct verification. We consider the following two sets:

1. 1.

   Structured aoki-multipliers [10]: This set of benchmarks is generated by combining different architectures for PPG, PPA, and FSA²²2PPG: simple (sp), Booth encoding (bp); PPA: Array (ar), Wallace tree (wt), Balanced delay tree (bd), Overturned-stairs tree (os), Dadda tree (dt), (4;2) compressor tree (ct), (7,3) counter tree (cn), Red. binary addition tree (ba); FSA: Ripple-carry (rc), Carry look-ahead (cl), Ripple-block carry look-ahead (rb), Block carry look-ahead (bc), Ladner-Fischer (lf), Kogge-Stone (ks), Brent-Kung (bk), Han-Carlson (hc), Conditional sum (cn), Carry select (cs), Carry-skip fix size (csf), Carry-skip var. size (csv), yielding 192 structured multiplier architectures. All of these circuits have an input bit-width of 64 and consist of $\mathrm{38\hspace{0.17em}000}$ to $\mathrm{52\hspace{0.17em}000}$ nodes.

2. 2.

   Synthesized ABC-multipliers [1]: We generate a multiplier using ABC, consisting of a simple PPG, an array PPA, and a ripple-carry FSA for bitwidths 32, 64, and 128. We optimize the multipliers using four standard synthesis scripts (resyn, resyn2, resyn3, dc2) and a complex script that combines multiple techniques³³3-c "logic; mfs2 -W 20; ps; mfs; st; ps; dc2 -l; ps; resub -l -K 16 -N 3 -w 100; ps; logic; mfs2 -W 20; ps; mfs; st; ps; iresyn -l; ps; resyn; ps; resyn2; ps; resyn3; ps; dc2 -l; ps;". These 15 optimized benchmarks showcase the robustness of our approach. The node size ranges between $8000$ and $\mathrm{130\hspace{0.17em}000}$.

Our experiments are conducted on a cluster of dual-socket AMD EPYC 7313 @ 3.7GHz machines running Ubuntu 24.04. The time is listed in rounded seconds (wall-clock time). We set the time limit to $300\mathrm{s}$ and the memory limit to $\mathrm{25\hspace{0.17em}000}\mathrm{MB}$.

We have presented a hybrid approach for extracting linear polynomials from a set of polynomials. Our approach combines an FGLM-style linearization method with a guess-and-prove-style approach. We first present these algorithms at a general level before instantiating them for circuit verification. Our experimental evaluation shows that we outperform existing linearization techniques based on Gröbner bases. In the future, we aim to further improve our tool with more sophisticated algorithms for subcircuit detection. We also envision that our methods have applications beyond circuit verification, such as equivalence checking.