Das Kapitel geht den Herausforderungen bei der Verifizierung arithmetischer Schaltkreise nach, insbesondere in sicherheitskritischen Anwendungen wie Kryptographie und Signalverarbeitung. Es unterstreicht die Grenzen traditioneller Methoden wie der SAT-Lösung und der binären Entscheidungsdiagramme (BDDs), wenn es um die komplexen nichtlinearen Strukturen arithmetischer Schaltkreise geht. Im Mittelpunkt steht dabei die Nutzung von Gröbner-Grundlagen, einem mathematischen Konstrukt, das ein Entscheidungsverfahren für die Solidität und Vollständigkeit des Verifikationsprozesses bietet. Das Kapitel stellt einen neuartigen Ansatz vor, der den Rechenaufwand von der Neuschreibung der Spezifikation auf die Neuschreibung der Gröbner-Basis selbst verlagert und eine stufenbasierte Terminologie vorschreibt, um den Grad während des Reduktionsprozesses zu begrenzen. Diese Methode ist theoretisch fundiert und wird anhand einer Reihe von Multiplikatoren-Benchmarks praktisch bewertet, was vielversprechende Ergebnisse zeigt. Das Kapitel behandelt auch die Vorverarbeitung und das Umschreiben von Algorithmen, die den Reduktionsprozess optimieren und damit einen bedeutenden Beitrag im Bereich der formalen Verifikation leisten.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
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 using polynomials that automatically generate a Gröbner basis with respect to a lexicographic term ordering. Correctness of the circuit is derived by computing the polynomial remainder of the specification. However, the main obstacle is the monomial blow-up during the reduction, as the degree can increase.
In this paper, we investigate an orthogonal approach and focus the computational effort on rewriting the Gröbner 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.
1 Introduction
Formal verification techniques based on algebraic reasoning have emerged as highly effective tools for verifying hardware, particularly in the context of verifying arithmetic circuits on the gate-level. As digital systems become more complex, ensuring the correctness of such circuits is paramount, especially in safety-critical applications like cryptography and signal processing to prevent a repetition of infamous failures, such as the Pentium FDIV bug [32]. Established methods based on satisfiability solving (SAT) [4], or binary decision diagrams (BDDs) [7] often struggle with the complex non-linear structure of arithmetic circuits. In contrast, formal verification techniques based on theorem provers [33] or computer algebra, specifically those leveraging Gröbner bases, offer an effective alternative and have made significant progress in recent years [18, 21, 22, 29].
In the algebraic method, circuits are given as and-inverter graphs (AIG) [23]. The graph is encoded as a set of polynomials, which are sorted according to a lexicographic term ordering, where for each gate in the circuit the output variable is always greater than the input variables of the gate. Hence, the leading terms of the polynomial equations consist of single variables that are mutually disjoint. This property is called unique monic leading term (UMLT) in [18].
Anzeige
If such an ordering is chosen, the polynomials automatically form a Gröbner basis [5]. Informally said, a Gröbner basis is a mathematical construct that offers a decision procedure that guarantees soundness and completeness of the verification process. The correctness of the circuit is determined by computing the unique polynomial remainder of the specification polynomial, which represents the intended functionality of the circuit, modulo the Gröbner basis. The circuit fulfills the specification if, and only if, the final remainder is zero [19].
However, a major practical obstacle in using a lexicographic term ordering is the significant computational effort during the reduction process, as the degree can increase. More precisely the size of the intermediate reduction results generally increases, since the tails of the polynomials in the Gröbner basis have a higher degree than their leading terms. This is often deferred to as monomial blow-up. A study in [28] showed that the intermediate reduction results for 16-bit multipliers can have more than \(10^6\) monomials. To address this challenge, various preprocessing and rewriting algorithms have been developed, which syntactically or semantically analyze the input circuit to remove redundant information from the polynomial encoding, ultimately optimizing the reduction process and improving the efficiency of the verification.
Related Work. Advanced reduction engines designed for the automatic algebraic verification of multipliers given as AIGs are implemented in tools such as DynPhaseOrderOpt [21], DyPoSub [29], and AMulet2 [17, 18], including its variant TeluMA [15]. In [17, 18] SAT solving is used to rewrite certain parts of the multiplier before applying an incremental column-wise verification algorithm. In a follow-up work [15] the usage of the external SAT solver could be removed by using a sophisticated algebraic encoding that also takes the polarity of literals into account. These techniques have been further enhanced by parallelization [26] and equivalence checking-based verification [24].
In [29], the authors present a dynamic rewriting approach. They decide on the reduction order on the fly and backtrack if the size of intermediate reduction results exceeds a predetermined threshold. In [21], the authors revisit and improve upon [29] by incorporating mixed signals in their encoding.
Anzeige
While all of the discussed approaches employ various preprocessing and rewriting techniques, they share a common characteristic: they all rely on a lexicographic term ordering. None of the related works have explored alternative term orderings, such as those that prioritize degree-based sorting to limit the degree during the reduction process.
Our contribution. In this paper, we propose an alternative, orthogonal strategy that shifts the focus of the computational effort from rewriting the specification to rewriting the Gröbner basis itself. We impose a different term ordering that takes their degree into account. The approach is based on the following observation:
Our first contribution is to derive the theoretical foundations of this observation, including a technical theorem that proves its soundness and completeness.
However, the computation of a single Gröbner basis for the whole circuit is practically infeasible due to the large number of variables and more importantly the degree of the underlying ideal. Our second contribution is a practical algorithm that splits the computation of the Gröbner basis into multiple smaller more manageable sub-problems. We evaluate our approach on a set of benchmarks for multiplier verification. The experimental results are promising and indicate that our approach offers a valuable addition to existing algebraic verification techniques.
The remainder of the paper is organized as follows. In Section 2 we introduce the necessary preliminaries. In Section 3 we show the theory of our approach and prove the soundness and completeness. We present a practical verification algorithm in Section 4, and discuss its implementation and the experimental evaluation in Section 5 before we conclude the paper in Section 6.
2 Preliminaries
In the first part of the preliminaries, Section 2.1, we introduce the theory of Gröbner bases following [5, 6, 8] and discuss key properties that are important for our approach. In the second part, Section 2.2, we present the necessary background on AIGs and how we can encode these graphs using polynomial equations.
2.1 Gröbner Basis
Definition 1
(Term, Monomial, Polynomial, see [8, Chap. 2, Sec. 2, Def. 7)]). Let \(X = (x_1,\dots ,x_n)\) be a set of variables and \(\mathbb {K}\) be a field. A monomial is a product of the form \(x_1^{e_1}\cdots x_n^{e_n}\), with exponents \(e_1,\dots ,e_n \in \mathbb {N}_0\). The set of all monomials is represented by [X]. A term is a monomial multiplied by a constant, written as \(\alpha x_1^{e_1}\cdots x_n^{e_n}\) with \(\alpha \in \mathbb {K}\). A polynomialp is a finite sum of such terms. We denote the number of terms in p by \({{\,\textrm{size}\,}}(p)\).
Throughout this section let \(\mathbb {K}[X]=\mathbb {K}[x_1,\dots ,x_n]\) denote the ring of polynomials in variables \(x_1,\dots ,x_n\) with coefficients in the field \(\mathbb {K}\). We write polynomials in their canonical form. That is, monomials with equal monomials are merged by adding their coefficients; and terms with coefficients equal to zero are removed.
Definition 2
(Degree). The degree of a monomial \(\sigma = x_1^{e_1}\cdots x_n^{e_n}\) is the sum of its exponents, i.e., \(\deg (\sigma ) = |\sigma | = \sum _{i=1}^{n}{e_i}\). The degree of a polynomial is the maximum degree of its terms.
The terms within a polynomial are sorted according to a total order to ensure a consistency for algebraic operations.
Definition 3
(Monomial Order). A monomial order is a total order \(\prec \) such that for all distinct monomials \(\sigma _1,\sigma _2\) we have (i) \(\sigma _1 \prec \sigma _2\) or \(\sigma _2 \prec \sigma _1\), (ii) every non-empty set of monomials has a smallest element and (iii) \(\sigma _1\prec \sigma _2\Rightarrow \tau \sigma _1\prec \tau \sigma _2\) for any term \(\tau \).
Definition 4
(Lexicographic Order, see [8, Chap. 2, Sec. 2, Def. 3]). Let \(\sigma _1= x_1^{u_1}\cdots x_n^{u_n}\) and \(\sigma _2= x_1^{v_1}\cdots x_n^{v_n}\) be two monomials. We say that \(\sigma _1 \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\sigma _2\), if there exists an index i such that with \(u_j = v_j\) for all \(1\le j<i\), and \(u_i<v_i\).
Definition 5
(Degree Reverse Lexicographic Order, see [8, Chap. 2, Sec. 2, Def. 6]). Let \(\sigma _1= x_1^{u_1}\cdots x_n^{u_n}\) and \(\sigma _2= x_1^{v_1}\cdots x_n^{v_n}\) be two monomials. We say that \(\sigma _1 \mathrel {\prec _{{{\,\textrm{drl}\,}}}}\sigma _2\), if \(|\sigma _1|<|\sigma _2|\) or if \(|\sigma _1|=|\sigma _2|\) and there exists an index i such that \(u_j = v_j\) for all \(i<j\le n\), and \(u_i>v_i\).
Since every polynomial \(p \in \mathbb {K}[X]\) contains only a finite number of monomials, and these terms are sorted according to a fixed total order, we can identify the largest monomial in p. This is referred to as the leading monomial of p and denoted as \({{\,\textrm{lm}\,}}(p)\). If \(p=c\tau + \cdots \) and \({{\,\textrm{lm}\,}}(p)=\tau \), then \({{\,\textrm{lc}\,}}(p)=c\) is called the leading coefficient and \({{\,\textrm{lt}\,}}(p)={{\,\textrm{lc}\,}}(p){{\,\textrm{lm}\,}}(p)=c\tau \) is called the leading term of p. The tail of p is defined by \({{\,\textrm{tail}\,}}(p) = p-{{\,\textrm{lt}\,}}(p)\).
Definition 6
(Ideal). A nonempty subset \(I\subseteq \mathbb {K}[X]\) is called an ideal if
$$ \forall \,u,v\in I: u+v\in I \quad \text { and }\quad \forall \,w\in \mathbb {K}[X]\ \forall \,u\in I: wu\in I. $$
If \(I\subseteq \mathbb {K}[X]\) is an ideal, then a set \(G=\{g_1,\dots ,g_m\}\subseteq \mathbb {K}[X]\) is called a basis of I if \(I=\{h_1g_1+\cdots +h_mg_m\mid h_1,\dots ,h_m\in \mathbb {K}[X]\}\), i.e., if I consists of all the linear combinations of \(g_i\) with polynomial coefficients. We denote this by \(I= \langle G\rangle \) and say I is generated by G.
An ideal \(I=\langle G\rangle \subseteq \mathbb {K}[X]\) can be interpreted as an equational theory, where the basis \(G=\{g_1,\dots ,g_m\}\) serves as the set of axioms. The ideal \(I = \langle G\rangle \) consists of precisely those polynomials f for which the equation \(f=0\) can be derived from the axioms \(g_1=\cdots =g_m=0\) through repeated application of the rules \(u=0\wedge v=0\Rightarrow u+v=0\) and \(u=0\Rightarrow wu=0\).
To check whether a polynomial \(f \in \mathbb {K}[X]\) is contained in an ideal I, we want to solve the so-called ideal membership problem: Given a polynomial \(f\in \mathbb {K}[X]\) and an ideal \(I= \langle G\rangle \subseteq \mathbb {K}[X]\), determine if \(f \in I\).
Definition 7
(Remainder). The process of finding a remainder with respect to a set of polynomials G is equal to computing the remainder of a polynomial division, but extended to multiple divisors, until no further division is possible. The result is a polynomial that represents the equivalent class modulo the ideal generated by G. We write \(p \rightarrow _G g\) to denote that g is the polynomial remainder of p modulo G and we also say “p is reduced by G”.
In general, an ideal I has many bases that generate I. We are particularly interested in bases with certain structural properties that allow to uniquely answer the ideal membership problem. Such bases are called Gröbner bases [5].
Lemma 1
(see [8, Chap. 2, Sec. 5, Cor. 6]). Every ideal \(I \subseteq \mathbb {K}[X]\) has a Gröbner basis w.r.t. a fixed total order.
Given an arbitrary basis of an ideal, a Gröbner basis can be computed using Buchberger’s algorithm that repeatedly computes so-called S-Polynomials. These S-Polynomials are reduced by the polynomials that are already in the current basis, i.e., calculating the remainder of polynomial division, and non-zero remainders are added to the ideal basis. These steps are repeated until the basis is saturated. If all S-Polynomials reduce to zero the set of ideal generators is a Gröbner basis [5]. Generally, Buchberger-like algorithms for computing Gröbner bases, such as Buchberger’s seminal algorithm [5] or Faugère’s \(\textrm{F}_4\) [9] algorithm, have a worst-case time complexity double exponential in the number of variables, because of the size of the output [30]. Still, in practice, these algorithms behave in general way better for \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\) than for other monomial orders, such as \(\mathrel {\prec _{{{\,\textrm{lex}\,}}}}\).
We will not introduce this process more formally, as we will treat the computation of a Gröbner basis as a black-box technique in our approach. The following properties are more important for us.
Lemma 2
(see [8, Chap. 2, Sec. 6, Prop. 1]). If \(G = \{g_1,\ldots ,g_m\}\) is a Gröbner basis, then every \(f\in \mathbb {K}[X]\) has a unique polynomial remainder r with respect to G. Furthermore, it holds that \(f-r \in \langle G\rangle \), which implies that f is contained in the ideal \(I=\langle G\rangle \) if, and only if, \(f \rightarrow _G 0\).
Depending on the information one seeks, some Gröbner bases are more useful than others. Gröbner bases w.r.t. \(\mathrel {\prec _{{{\,\textrm{lex}\,}}}}\) are the tool of choice for solving polynomial systems but are, in general, more expensive to compute than degree-based Gröbner bases. Yet, change of order algorithms, such as the seminal FGLM one [11] can convert a Gröbner basis into another one for different order. In our setting of verifying AIG the complexity would be in \(O(n 2^{3 n})\), where n is the number of input variables of the AIG. Hence, for large n, this is impractical. Variants of FGLM exploiting the structure of the input and output Gröbner bases under some genericity assumptions exist, we can mention [2, 10, 12, 31], but they are mostly designed for solving polynomial systems. As a consequence, they consider the input Gröbner basis to be for a degree-based order, such as \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\), and the output Gröbner basis to be for \(\mathrel {\prec _{{{\,\textrm{lex}\,}}}}\).
2.2 And-Inverter Graphs
An and-inverter graph (AIG) [23] is a special case of a directed acyclic graph (DAG). They are useful tools to represent Boolean functions and logic circuits and provide a compact and efficient way to describe logical expressions.
Definition 8
(AIG). An AIG operates over Boolean variables. Every node expresses a logical conjunction between its two input variables, which are depicted by incoming edges in the lower part of the node. We distinguish two types of inputs, primary inputs (of the graph) and intermediate nodes. Outputs of the node are represented by an edge in the upper half. If an edge is marked, it indicates that the variable is negated.
Definition 9
(Specification). The specification of an AIG is a polynomial equation \({\mathcal {S}}\in \mathbb {K}[X]\) that relates the outputs of an AIG to its primary inputs.
Together with the specification polynomial, we fix the polynomial ring \(\mathbb {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 \(\mathbb {B}[X]\), but may include different coefficient domains, such as integers or rationals.
Definition 10
(Gate Polynomials). Each node in an AIG can be encoded by a corresponding polynomial equation that models the logical conjunction. Nodes in an AIG raise four types of equations, depending if either none, the first, the second, or both inputs are negated. Let g be an AIG node with inputs a, b:
The correctness of the encoding can easily be checked by truth tables. Furthermore, observe that the degree of the gate polynomials is always two.
Definition 11
(Boolean Input Polynomial). For every primary input \(a_i\) of the AIG we define a corresponding Boolean input polynomial\(a_i(a_i-1) = a_i^2-a_i = 0\) that encodes that the variable can only take the values 0 and 1.
As we will only consider polynomial equations with right hand side zero, we will from now on shorten our notation and write “f” instead of “\(f =0\)”.
Fig. 1.
AIG and polynomial encoding of a 2-bit multiplier in the ring \(\mathbb {Q}[X]\).
Example 1
Figure 1 shows an AIG representing a 2-bit multiplier. We denote the primary inputs by \(a_0, a_1, b_0, b_1\) and outputs by \(s_0, s_1, s_2, s_3\). The internal nodes are denoted by \(\ell _i\), with subscript i corresponding to the number of the respective AIG node. The right hand side of Figure 1 lists the gate constraints as well as the corresponding gate polynomials, which are derived using the encoding presented in Def. 10. We furthermore list the Boolean input polynomials (Def. 11) and the specification polynomial \({\mathcal {S}}\in \mathbb {Q}[X]\), which relates that \(S = A \cdot B \), for \(S = \sum _{i=0}^3 2^is_i\), \(A = \sum _{i=0}^1 2^ia_i\), and \(B = \sum _{i=0}^1 2^ib_i\).
3 Verification using Degree Reverse Lexicographic Order
In this section we will lay out the theoretical foundation of our proposed approach for extracting linear relations from the Gröbner basis that is used for reduction.
Existing algebraic verification techniques for acyclic graphs encode the circuit as a polynomial using a lexicographic term ordering where the variables are sorted according to a reverse topological term ordering (RTTO) [27]. This has the benefit that due to repeated application of Buchberger’s product criterion, see [8, Chap. 2, Sec. 10, Prop. 1], the set of gate polynomials together with the Boolean input polynomials automatically form a Gröbner basis [19]. Since the leading terms of the gate polynomials consist of one single variable, polynomial division comes down to substitution. The variables in the specification are substituted by the corresponding tails of the gate polynomials until no further rewriting is possible. The graph fulfills its specification if, and only if, the final result is zero.
Generally, this implies that the degree of the intermediate reduction results increases, since the tails of the gate polynomials have a higher degree than their linear leading terms. Substituting those variables in non-linear monomials has the potential to lead to a monomial blow-up during the reduction.
Example 2
Consider again the polynomials of Example 1. Initially \({{\,\textrm{size}\,}}({\mathcal {S}}) = 8\) and \(\deg ({\mathcal {S}}) = 2\). After four rewriting steps we have the following intermediate reduction result: \({\mathcal {S}}\rightarrow _{\{g_1,g_2,g_3,g_4\}} 4\ell _{24}\ell _{22}\ell _{16}-4\ell _{24}\ell _{22}-4\ell _{24}\ell _{16}+8\ell _{24}-4\ell _{22}\ell _{16}+4\ell _{22}+2s_{1}+4\ell _{16}+s_0 - 4a_1b_1 - 2a_1b_0-2a_0b_1-a_0b_0\) which has degree 3 and consists of 13 monomials.
We will now impose a different ordering on the set of gate polynomials that takes the degree of the polynomials into account. That is, we compute a Gröbner basis based on the degree reverse lexicographic monomial ordering, where the monomials in a polynomial are first sorted according to their degree.
Our approach is based on the following result that we prove in Theorem 1: If the specification polynomial is linear, then the ideal membership of the specification can be decided using only the linear polynomials of the Gröbner basis.
We linearize the specification by replacing all non-linear monomials \(\sigma _i\) in \({\mathcal {S}}\) with new extension variables \(t_i\). For each replacement we generate a new polynomial constraint \(t_i - \sigma _i\) and add it to the set of gate polynomials. The idea of linearization is, for instance, already used in [25] in the context of cutting planes.
The next lemma proves that if the specification \({\mathcal {S}}\) is contained in the ideal generated by the gate polynomials, then the linearized specification \({\mathcal {S}}_{{{\,\textrm{lin}\,}}}\) is contained in the ideal generated by the gate polynomials and extension polynomials.
Lemma 3
Let \(p \in \mathbb {K}[X]\), \(I \subseteq \mathbb {K}[X]\). Let \(\Sigma = \{t_i - \sigma _i \mid t_i \notin X \wedge \sigma _i \in p \wedge \deg (\sigma _i) > 1 \}\). Let \(p_{{{\,\textrm{lin}\,}}}\) be the polynomial where every non-linear monomial of p is replaced by a corresponding extension variable \(t_i\). Then we have \(p \in I\) if, and only if, \(p_{{{\,\textrm{lin}\,}}} \in I + \langle \Sigma \rangle \).
Proof
Let \(p=\sum _{\sigma _i\in p}c_i \sigma _i\), where the \(c_i\)’s are in \(\mathbb {K}\). By definition, we can write \(p_{{{\,\textrm{lin}\,}}}=\sum _{\sigma _i\in p}c_i t_i\). Thus, \(p_{{{\,\textrm{lin}\,}}} = \sum _{\sigma _i\in p}c_i(t_i - \sigma _i) + \sum _{\sigma _i\in p}c_i\sigma _i\). By hypothesis, the first sum is in \(\langle \Sigma \rangle \) and the second one, which is p, only depends in variables X. Therefore, if \(p\in I\), then \(p_{{{\,\textrm{lin}\,}}}\in I+\langle \Sigma \rangle \). Conversely, if \(p_{{{\,\textrm{lin}\,}}}\in I+\langle \Sigma \rangle \), then \(p\in (I+\langle \Sigma \rangle )\cap \mathbb {K}[X]=I\) by construction of \(I+\langle \Sigma \rangle \).
We now show soundness and completeness of our observation. That is, if we want to show ideal membership of a linear polynomial, the Gröbner basis of the ideal contains a set of linear polynomials \(G_1\) that suffice for deriving the ideal membership, all non-linear polynomials of the Gröbner basis can be neglected. This will shift the computational difficulties from the reduction to the Gröbner basis generation.
Theorem 1
Let \(p \in \mathbb {K}[X]\) with \(\deg (p) = 1\), \(I \subseteq \mathbb {K}[X]\) be an ideal. Let G be a Gröbner basis of I with respect to \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\) and let \(G_1 = \{g \in G \mid \deg (g) \le 1\}\). We have \(p \in I\) if, and only if, \(p \rightarrow _{G_1} 0\). In particular, \(p = \alpha _1g_1 + \cdots + \alpha _mg_m\) with \(g_i \in G_1\), \(\alpha _i \in \mathbb {K}\).
Proof
First, let us observe that if \(G_1\) contains a non-zero constant polynomial, then \(I=\mathbb {K}[X]\) and p necessarily reduces to 0 by \(G_1\).
We now assume that \(G_1\) only contains polynomials of degree 1. For \(g\in G_1\), we write \(g={{\,\textrm{lt}\,}}(g)+{{\,\textrm{tail}\,}}(g)\). Because polynomials in \(G_1\) are ordered with respect to \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\), we have \(\deg ({{\,\textrm{lm}\,}}(g))=1\) and \(\deg ({{\,\textrm{tail}\,}}(g))\le 1\). Since \(\deg ({{\,\textrm{lm}\,}}(p))=1\) the division algorithm for computing the reduction of p by G, see [8, Chap. 2, Sec. 3], will only select polynomials in G whose leading monomials also have degree 1, i.e. those in \(G_1\). The reduction step will replace p by \(p-\alpha _i g_i={{\,\textrm{tail}\,}}(p)-\alpha _i{{\,\textrm{tail}\,}}(g_i)\), for \(\alpha _i\in \mathbb {K}^*\) and some \(g_i\), which has degree less or equal to 1.
Since \(p\in I\) if, and only if, \(p\rightarrow _G 0\), we have \(p\in I\) if, and only if, \(p\rightarrow _{G_1} 0\).
We emphasize that the theory, and in particular the result of Theorem 1, can be applied to general DAGs. The key property of the graph is that it must be acyclic. If it has cycles one cannot canonically compare the variables, hence it is not possible to derive a total term order and compute a Gröbner basis.
The conclusion of Theorem 1 moreover shows that we can significantly simplify the algorithm for checking the ideal membership of \({\mathcal {S}}\). Instead of repeated polynomial substitution, with potential non-linear intermediate reduction results, we pick \(g_i \in G_1\), such that \({{\,\textrm{lm}\,}}(g_i) = {{\,\textrm{lm}\,}}({\mathcal {S}})\), multiply \(g_i\) by a constant \(\alpha _i\) such that \({{\,\textrm{lc}\,}}({\mathcal {S}}) = -\alpha _i{{\,\textrm{lc}\,}}(g_i)\) and add those two polynomials. Hence, we have replaced polynomial division by linear polynomial operations.
Therefore, we can apply the following approach to verify that an AIG fulfills its specification, see Alg. 1. We first encode the graph as a set of polynomials \(G_{{{\,\textrm{init}\,}}}\) (line 1), and linearize the specification (line 2) as described in Lemma 3. The set \(G_{{{\,\textrm{ext}\,}}}\) contains the extension polynomials. In the next step we compute a Gröbner basis w.r.t. \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\) (line 3) and extract the linear polynomials \(G_1\) (line 4). We calculate the remainder of the specification modulo the linear elements of the Gröbner basis (lines 5–8) until no further reduction is possible and return whether the final result is zero. The correctness of Alg. 1 follows from Theorem 1.
Algorithm 1
Linear Gröbner basis reduction
Example 3
Consider again the AIG of Example 1. First of all we define four extension variables \(t_{ij}\) to encode the non-linear terms \(a_ib_j\) for \(i,j \in \{0,1\}\) and rewrite the specification to \(8s_3+4s_2+2s_1+s_0 - 4t_{11} - 2t_{10}-2t_{01}-t_{00}\). The four polynomial equations \( t_{ij} - a_ib_j\) are added to the set of gate polynomials and we compute a Gröbner basis w.r.t. \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\). The full Gröbner basis consists of 52 polynomials. Important for us are the first thirteen elements of the Gröbner basis, as those are the linear polynomials \(G_1\):
We derive that \({\mathcal {S}}\in \langle G_1\rangle \) as \({\mathcal {S}}= 8g_{13}+4g_{12}+4g_{11}+2g_7+2g_6+g_2+g_1\).
In practice, however line 3 of Alg. 1 turns out to be a bottleneck, since computing a single \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis does not scale for larger AIGs.
We have also seen in Example 1 that 39 out of 52 polynomials in the computed Gröbner basis are non-linear. While these polynomials are needed to compute the full Gröbner basis of the ideal, they are not required for solving the ideal membership problem of the linear specification. Furthermore, from the 13 linear polynomials, only 7 are used to generate the specification. Hence, our generated Gröbner basis contains redundant and/or useless information. We will now discuss a method to reduce the overhead by computing local Gröbner bases.
4 Locally extracting Linear Polynomials
The core idea of the optimized approach is to start from a \(\mathrel {\prec _{{{\,\textrm{lex}\,}}}}\)-Gröbner basis and incrementally extract linear polynomials from a smaller set of gate polynomials instead of computing a single full \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis for the whole input AIG. The algorithm is outlined in Alg. 2 and will be explained in more detail throughout the remainder of this section.
In a nutshell, we first encode the circuit using a lexicographic term ordering (line 1) and linearize the specification polynomial (line 2) with respect to the given circuit. After some preprocessing where we extract easily derivable linear polynomials (line 3), we rewrite the specification by generating linear polynomials on the fly (lines 4–9). We pick the gate polynomial p that has the same leading term as the intermediate reduction result (line 5) and compute a \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis for a sub-circuit of C that includes p (line 6) to receive the linearized polynomial \(p_{{{\,\textrm{lin}\,}}}\) that we use for reducing the specification (line 7). Let us now go into more detail of every step.
Encoding. The AIG is encoded using gate polynomials and Boolean input polynomials as described in Definitions 10 and 11 using a lexicographic term ordering. We choose a row-wise variable ordering that sorts variables based on their distance to the inputs. If nodes have an equal distance, we sort according to the value of the AIG node. For example, we would sort the variables in Example 1 as \(a_0 \mathrel {\prec _{{{\,\textrm{lex}\,}}}}b_0 \mathrel {\prec _{{{\,\textrm{lex}\,}}}}a_1 \mathrel {\prec _{{{\,\textrm{lex}\,}}}}b_1 \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{10} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{12} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{14} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{22} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}s_{0} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{16} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{18} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{20} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{24} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{26} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}\ell _{28} \mathrel {\prec _{{{\,\textrm{lex}\,}}}}s_1 \mathrel {\prec _{{{\,\textrm{lex}\,}}}}s_3 \mathrel {\prec _{{{\,\textrm{lex}\,}}}}s_2\). In this order the output variable of a gate is always greater than its input variables, which automatically generates a \(\mathrel {\prec _{{{\,\textrm{lex}\,}}}}\)-Gröbner basis.
Theorem 4 in [19] has shown that we can locally rewrite elements of the \(\mathrel {\prec _{{{\,\textrm{lex}\,}}}}\)-Gröbner basis without jeopardizing the Gröbner basis property as long as the leading monomials remain the same. We apply the same technique and locally rewrite gate polynomials from quadratic to linear polynomials that will be used in the reduction.
Linearization of the Specification. Lemma 3 provides us with a methodology on how to linearize the specification \({\mathcal {S}}\) by introducing extension variables to represent non-linear terms. However, some of the terms might already be contained in the polynomial encoding of the circuit. For those terms we can simply use the corresponding leading term in the specification. We first swipe through the set of gate polynomials and check whether the non-linear tail of a gate polynomial is contained in the specification. If this is the case, we replace the non-linear term by the corresponding leading term.
For instance, in Example 3 we have the gate polynomial \(\ell _{22}-a_1b_1\). Hence, we do not require the extension variable \(t_{11}\) to linearize \({\mathcal {S}}\). This equality \(\ell _{22} = t_{11}\) is also contained as polynomial \(g_8\) in the computed \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis.
All non-linear terms of \({\mathcal {S}}\) that cannot be linearized using gate polynomials we introduce extension variables as described in Section 3.
At this point, our encoding consists of a linear specification polynomial and a set of quadratic gate polynomials and Boolean input polynomials that generate a Gröbner basis w.r.t. a lexicographic term ordering. The following subsections present how we linearize elements of the Gröbner basis.
4.1 Preprocessing
The goal of preprocessing is to eliminate variables and derive linear polynomials in the \(\mathrel {\prec _{{{\,\textrm{lex}\,}}}}\)-Gröbner basis that can be identified using simple heuristics. We employ three steps of rewriting, depicted in Alg. 3.
Algorithm 3
Preprocessing
Merge Nodes with Equal Inputs. If multiple AIG nodes \(\ell _i, \ell _j\) have the same inputs a, b, we can express one gate polynomial using the other. For instance, in our running Example 1 the nodes \(\ell _{24} = \ell _{22}\ell _{16}\) and \(\ell _{26}=(1-\ell _{22})(1-\ell _{16})\) would be such a set of AIG nodes.
Every gate polynomial of an AIG node has degree two, and the quadratic term is the product of the input nodes. Hence, the non-linear term in those gate polynomials that have the same inputs is the same. We remove the non-linear term of the topologically larger polynomial by adding or subtracting the smaller polynomial. For instance, we derive \(\ell _{26} - \ell _{24} + \ell _{22} + \ell _{16} - 1\).
Furthermore, assume two gates \(\ell _i\) and \(\ell _j\) both have input variables a, b. If at least one input has a different polarity in \(\ell _i\) and \(\ell _j\), we immediately can derive that the product \(\ell _i\ell _j\) is equal to zero. To see this, let \(\ell _i - \bar{a}\bar{b}\), \(\ell _j - \hat{a}\hat{b}\) be the corresponding gate polynomials, where \(\bar{a}\) and \(\hat{a}\) represent the polarity of a. We have \(\ell _i\ell _j = \bar{a}\bar{b}\hat{a}\hat{b} = 0\), since \((\bar{a} = 1-\hat{a}) \vee (\bar{b} = 1-\hat{b})\) holds. Thus, we can always remove the term \(\ell _i\ell _j\) in a possible parent node, for instance the monomial \(\ell _{26}\ell _{24}\) in \(\ell _{28}\) in Example 1 can be removed.
Eliminate Positive Nodes. In this step we eliminate nodes which are only non-negated inputs to other nodes in the graph. This heuristic was already considered in [15] to introduce a possible sharing of nodes. Since this heuristic is only applied on positive inputs, we can simply replace every occurrence of the node by the corresponding tail in the gate polynomial of the parent node. This will increase the degree of the parent polynomial, but will not increase the number of terms. We can check whether parts of the new tail term of the parent are equal to the tail term of another gate polynomial. If yes, we can reduce the tail term and include the leading term. This will decrease the temporal increase of the polynomial degree and furthermore will impose a node sharing which will be useful in later Gröbner basis computations. For instance, consider polynomials \(f-da, e-ca, d-cb\). We can derive \(f-cba = f-eb\).
Propagating Equivalent Nodes. If at any point in the rewriting we derive a linear polynomial of the form \(\ell _i - \ell _j\) or \(\ell _i + \ell _j -1\) we know that \(\ell _i\) is equal to either \(\ell _j\) or to its negation \(1-\ell _j\). We propagate this information by eliminating the topologically larger node \(\ell _i\) from the polynomial encoding. We choose to eliminate \(\ell _i\) and not \(\ell _j\) in order to not mess up the reverse topological term ordering for parent nodes of \(\ell _j\). Propagation of equivalent nodes may not directly lead to linear gate polynomials, but helps to reduce the overall number of variables.
4.2 Linear Reduction
After preprocessing we repeatedly rewrite the linearized specification by the polynomial p in the Gröbner basis that has the same leading monomial as the specification (line 5 in Alg. 2). For doing so, we need to linearize p. The pseudo-code is listed in Alg. 4. By Theorem 1, we know that a full \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis of a circuit C must contain a linear polynomial \(p_{{{\,\textrm{lin}\,}}}\) with the same leading monomial as p. If this condition is not met, then the circuit does not satisfy the specification, as we cannot further reduce \({\mathcal {S}}\).
Algorithm 4
Linearize-Single-Polynomial
However, we do not want to compute a full \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\) Gröbner basis. Our goal is to make the Gröbner basis just big enough such that it contains a linear polynomial \(p_{{{\,\textrm{lin}\,}}}\) with leading term v. Let \(v = {{\,\textrm{lm}\,}}(p)\). We aim to compute a Gröbner basis w.r.t. a \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-ordering for a sub-circuit \(C_{v,d}\) of C. The sub-circuit \(C_{v,d}\) is constructed by including v and all children nodes of v up to a maximum distance d. Initially, we set \(d=3\). The motivation for this threshold is that our preprocessing techniques already generates most linear polynomials detectable with \(d=2\). On the other hand we do not want to start with a larger value for d to keep the initial Gröbner basis computation as small as possible. If we encounter a child node that already has a linear polynomial representation, we do not further add its children. This allows us to avoid unnecessary computations by excluding parts of the circuit that have already been simplified. Additionally, we include all smaller sibling nodes of v. Siblings are nodes that share at least one child with v. Moreover, we collect all parent nodes whose children are already included in the collected set of nodes. This ensures that all relevant dependencies in the sub-circuit are captured. This set of nodes represents the part of the circuit on which we will compute a local \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis.
If this local Gröbner basis does not contain the expected linear polynomial, it suggests that the sub-circuit \(C_{v,d}\) is insufficient to capture the desired behavior. In such cases, we repeat the process for the sub-circuit \(C_{v,d+1}\), where we increase the distance d to add more nodes. Theoretically it would be very beneficial to cache the calls and reuse the computed Gröbner basis for \(C_{v,d}\) for the Gröbner basis computation of \(C_{v,d+1}\), however in practice most available Gröbner basis engines cannot exploit that a subset of the inputs is already Gröbner basis.
We continue with the iterative process of increasing d until either a linear polynomial is found, or, in the worst case we have computed a full \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis for all gate polynomials that are topologically smaller than v. If we still did not find a linear polynomial at this point, we know that the circuit is incorrect. This follows from Theorem 1.
While our approach guarantees the completeness of the verification process, it comes with a practical limitation: computational complexity. If the sub-circuit grows too large (i.e., if too many nodes need to be added to \(C_v\)), the computation of the \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis becomes infeasible in practice.
5 Experimental Evaluation
We evaluate our proposed approach on a set of multiplier benchmarks for different input bit-widths n. For all the circuits we have \({\mathcal {S}}= \sum _{i=0}^{2n+1} 2^is_i - (\sum _{i=0}^n 2^ia_i)\cdot (\sum _{i=0}^n 2^ib_i)\), hence choose \(\mathbb {K}= \mathbb {Q}\). Since all the leading coefficients of the gate polynomials are 1, the computation will stay in the ring \(\mathbb {Z}[X] \subseteq \mathbb {Q}[X]\) [18].
5.1 Implementation
We implement Alg. 2 in our tool MultiLinG [14, 16], written in C++. We employ the following features:
MultiLinG uses the polynomial arithmetic module from AMulet2 [17], which is targeted towards polynomial arithmetic where the variables represent Boolean values and the coefficients are integer values. In particular, the arithmetic engine automatically includes reasoning over the Boolean input polynomials, by reducing exponents, i.e., it calculates \(x\cdot x = x\) internally.
We sort the variables based on their minimum distance to the primary inputs to sort all extension variables next to the primary inputs, which gave us better practical results than the column-wise variable order from AMulet2.
As a consequence of the row-wise order, we do not apply an incremental column-wise reduction algorithm [19], but rewrite the complete specification.
For computing the \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis, we use the msolve [3] library. Since msolve is designed for general purposes, we have to explicitly provide the Boolean input polynomials.
If the distance of a node to the primary inputs is below six and the linearization of the individual polynomial fails, we switch to non-linear rewriting as a fall-back option. This threshold allows us to capture Booth encoding in our multiplier benchmarks. We empirically noticed that the linearization of Booth encodings requires a rather large \(\mathrel {\prec _{{{\,\textrm{drl}\,}}}}\)-Gröbner basis and it is computationally cheaper to use non-linear rewriting instead. However, switching to non-linear rewriting leads to a non-linear intermediate reduction result, meaning that we have to use non-linear rewriting also for the remainder of the circuit to maintain completeness.
In contrast to AMulet2, we do not support proof logging in MultiLinG at the moment, as we have not yet instrumented msolve to produce proofs in the PAC [20] format. This missing implementation is part of future work.
5.2 Setup
We run our experiments on a Intel i7-1260P CPU. The time is listed in rounded seconds (wall-clock time). We set the time limit to 300 s and the memory limit to 10000 MB. We compare MultiLinG against the algebraic approaches of AMulet2 [17], TeluMA [15], and DynPhaseOrderOpt (DPOO) [21]. The tools of related works [26] and [24] are not publicly available.
Benchmarks. We evaluate our approach on integer multiplier circuits. Multipliers consist of three main components: partial product generation (PPG), partial product accumulation (PPA), and a final-stage adder (FSA). Each component has optimized architectures to reduce space and delay.
Two encodings are frequently used for PPG: simple AND-gate-based generation or Booth encoding. In the former case, every partial product \(a_ib_j\) is explicitly computed, hence we do not require extension variables in our approach. For Booth encoding, we require extension variables as the partial products are internally combined. During PPA, partial products are accumulated, with the final two layers summed in the FSA.
In structured circuits, PPG, PPA, and FSA are clearly defined, benefiting tools like AMulet2 and TeluMA that require a clear cut between PPA and FSA to simplify the FSA. In synthesized circuits, gates are merged and rewritten to optimize the circuit, which blurs these component boundaries, and complicates direct verification. We consider two sets of benchmarks:
aoki-multipliers [13]: This set of benchmarks is generated by combining different architectures for PPG, PPA, and FSA1 , yielding 192 non-synthesized multiplier architectures with an input bit-width 64.
optimizedABC multipliers [1]: We generate multipliers in ABC consisting of a simple PPG, an array PPA and a ripple-carry adder as FSA for bit-widths 32, 64, and 128, and optimize all of them within ABC using five different types of standard synthesis scripts: resyn, resyn2, resyn3, dc2. We include a complex script that combines several synthesis techniques2. We include these 15 optimized benchmarks to demonstrate the robustness of our presented approach. Optimized benchmarks are particularly challenging as they cannot be fully decomposed into their building blocks.
All benchmarks model correct multipliers, i.e., the circuits fulfill the specification.
5.3 Results
Table 1.
Results on n-bit ABC benchmarks. TO \(:== >{300}\,s\); EE \(:==\) segfault.
Dummy
The results for the optimized ABC multipliers are shown in Table 1. The heuristics of AMulet2 and TeluMA are not robust for these benchmarks and produce time outs. DPOO and our tool MultiLinG are both able to solve all benchmarks within the time limit. We provide statistics on MultiLinG and show how often nodes with equal inputs are merged (“MergedN”), the number of eliminated positive nodes (“PosN”). We explicitly measure the time that is required by msolve. This time is included in the total computation time. Additionally we provide statistics on the msolve calls and list the total number (“#”), as well as the number of calls for each depth d and the average computation time per depth. For “resyn3” and “dc2” everything could be linearized via merging nodes. This is in high contrast to the aoki benchmarks, see Table 2 and we believe this is due to dense structure of the ABC graphs, which involve a higher sharing of nodes leading to more node pairs with equal children.
Fig. 2.
Results of aoki-benchmarks
Fig. 3.
MultiLinG versus DPOO
Table 2.
Results on solved aoki benchmarks.
Dummy
Figure 2 shows the results on the aoki-benchmarks. Both, TeluMA and AMulet2, are able to solve the complete benchmark set. DPOO solves 163 out of 192 benchmarks, whereas our approach is only able to solve 29 benchmarks. 106 benchmarks exceed the memory limit and 57 benchmarks exceed the time limit. Details on the solved instances are given in Table 2.
Although the number of solved instances is low for MultiLinG, we are able to solve 13 benchmarks that DPOO does not cover, see Figure 3. All those instances use a carry-lookahead adder (cl) as FSA, which includes sequences of OR-gates that lead to a monomial blow-up when rewritten. AMulet2 and TeluMA solve these benchmarks using either a SAT solver or polynomial rewriting to replace the FSA with an equivalent ripple-carry adder. In our approach these circuits benefit from rewriting positive nodes.
Table 2 provides additional insights and shows that for multipliers using a simple PPG between 65–86% of the computation time is spent in msolve. For multipliers using a Booth encoding (bp) this percentage is lower, as we switch to non-linear rewriting during the reduction. Column “Nlin” provides the percentage of “Nodes” that are reduced using non-linear rewriting.
Summarizing,AMulet2 andTeluMA are highly efficient on the structured circuits but are not robust on optimized benchmarks.DPOO andMultiLinG are both robust and complement each other on complex multiplier designs. Hence our proposed approach is a valuable addition to the algebraic verification landscape and will be even more powerful when combined with existing methods.
6 Conclusion
In this paper we have presented a novel technique to verify directed acyclic graphs using computer algebra. Our first contribution is a theoretical theorem that shows how we can perform the ideal membership test of a specification polynomial using only linear polynomial operations. Secondly, we discuss how we can apply this theorem in practice to overcome the overhead of computing a full Gröbner basis. We present a technique that incrementally computes Gröbner bases for small sub-graphs to extract the linear information of the polynomials. We have demonstrated the potential of our approach on a set of multiplier circuits that have been challenging to verify so far.
In the future we aim to turn the black-box Gröbner basis approach into a white-box and explore how we can derive the linear polynomials without the computation of a full Gröbner basis. We also envision equivalence checking as a potential application, as this restricts the computation to Boolean polynomials.
Acknowledgments
This research was supported by the Austrian Science Fund (FWF) [10.55776/ESP666], the joint ANR-FWF ANR-19-CE48-0015 ECARP and ANR-22-CE91-0007 EAGLES projects, the ANR-19-CE40-0018 De Rerum Natura project, and grants DIMRFSI 2021-02-C21/1131 of the Paris Île-de-France Region and FA8665-20-1-7029 of the EOARD-AFOSR.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
