Rectification of Arithmetic Circuits with Craig Interpolants in Finite Fields

Utkarsh Gupta, Irina Ilioea, Vikas Rao, Arpitha Srinath, Priyank Kalla, Florian Enescu

► To cite this version:

Utkarsh Gupta, Irina Ilioea, Vikas Rao, Arpitha Srinath, Priyank Kalla, et al. Rectification of Arithmetic Circuits with Craig Interpolants in Finite Fields. 26th IFIP/IEEE International Conference on Very Large Scale Integration - System on a Chip (VLSI-SoC), Oct 2018, Verona, Italy. pp.79-106, 10.1007/978-3-030-23425-6_5. hal-02321766

HAL Id: hal-02321766

https://inria.hal.science/hal-02321766

Submitted on 21 Oct 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Rectification of Arithmetic Circuits with Craig Interpolants in Finite Fields *

Utkarsh Gupta¹, Irina Ilioaea², Vikas Rao¹, Arpitha Srinath¹, Priyank Kalla¹, and Florian Enescu²

¹Electrical and Computer Engineering, University of Utah, Salt Lake City UT, USA

²Mathematics and Statistics, Georgia State University, Atlanta GA, USA
{utkarsh.gupta,vikas.k.rao,arpitha.srinath}@utah.edu
iilioaea1@student.gsu.edu,kalla@ece.utah.edu,fenescu@gsu.edu

**Abstract.** When formal verification of arithmetic circuits identifies the presence of a bug in the design, the task of rectification needs to be performed to correct the function implemented by the circuit so that it matches the given specification. In our recent work [26], we addressed the problem of rectification of buggy finite field arithmetic circuits. The problems are formulated by means of a set of polynomials (ideals) and solutions are proposed using concepts from computational algebraic geometry. Single-fix rectification is addressed – i.e. the case where any set of bugs can be rectified at a single net (gate output). We determine if single-fix rectification is possible at a particular net, formulated as the Weak Nullstellensatz test and solved using Gröbner bases. Subsequently, we introduce the concept of Craig interpolants in polynomial algebra over finite fields and show that the rectification function can be computed using algebraic interpolants. This article serves as an extension to our previous work, provides a formal definition of Craig interpolants in finite fields using algebraic geometry and proves their existence. We also describe the computation of interpolants using elimination ideals with Gröbner bases and prove that our procedure computes the smallest interpolant. As the Gröbner basis algorithm exhibits high computational complexity, we further propose an efficient approach to compute interpolants. Experiments are conducted over a variety of finite field arithmetic circuits which demonstrate the superiority of our approach against SAT-based approaches.

**Keywords:** Rectification, Arithmetic circuits, Gröbner bases, Craig interpolants

## 1 Introduction

The past decade has witnessed extensive investigations into formal verification of arithmetic circuits. Circuits that implement polynomial computations over large bit-vector operands are hard to verify automatically using methods such as SAT/SMT-solvers, decision diagrams, etc. Recent techniques have investigated the use of polynomial algebra and algebraic geometry techniques for their verification. These include verification of integer arithmetic circuits [1] [2] [3], integer modulo-arithmetic circuits [4], word-level

<footnote>* This research is funded in part by the US National Science Foundation grants CCF-1619370 and CCF-1320385.</footnote>
RTL models of polynomial datapaths [5] [6], finite field combinational circuits [7] [8]
[9], and also sequential designs [10]. A common theme among the above approaches is
that designs are modeled as sets of polynomials in rings with coefficients from integers
$\mathbb{Z}$, finite integer rings $\mathbb{Z}_{2^k}$, finite fields $\mathbb{F}_{2^k}$, and more recently also from the field of fractions $\mathbb{Q}$. Subsequently, the verification checks are formulated using algebraic geometry
[11] (e.g., the Nullstellensatz), and Gröbner basis (GB) theory and technology [12] are
used as decision procedures (ideal membership test) for formal verification.

While these techniques are successful in proving correctness or detecting the presence of bugs, the task of post-verification debugging, error diagnosis and rectification of arithmetic circuits has not been satisfactorily addressed. Debugging and rectification of arithmetic circuits is of utmost importance. Arithmetic circuits are mostly custom designed; this raises the potential for errors in the implementation, which have to be eventually rectified. Instead of redesigning the whole circuit, it is desirable to synthesize rectification sub-functions with minimal topological changes to the existing design – a problem often termed as *partial synthesis*. Moreover, the debug, rectification and partial synthesis problem is analogous to that of synthesis for Engineering Change Orders (ECO), where the current circuit implementation should be minimally modified (recified) to match the ECO-modified specification. The partial synthesis approach also applies here to generate ECO-patches for rectification.

The problem of debug, rectification and ECO synthesis has been addressed for
control-dominated applications and random-logic circuits, where the early develop-
ments of [13] [14] [15] were extended by [16] by formulating as CNF-SAT, and com-
puting rectification functions using *Craig Interpolants* [17] in propositional logic.

Craig Interpolation (CI) is a method in automated reasoning to construct and refine abstractions of functions. It is a logical tool to extract concise explanations for the infeasibility of a set of mutually inconsistent statements. As an alternative to quantifier elimination, CI finds application in verification as well as in partial synthesis – and therefore, in rectification. In propositional logic, they are defined as follows.

**Definition 1.1.** (Craig Interpolants) Let (A, B) be a pair of CNF formulas (sets of clauses) such that A ∧ B is unsatisfiable. Then there exists a formula I such that: (i) A ⇒ I; (ii) I ∧ B is unsatisfiable; and (iii) I refers only to the common variables of A and B, i.e. Var(I) ⊆ Var(A) ∩ Var(B). The formula I is called the **interpolant** of (A, B).

Despite these advancements in automated debugging and rectification of control and
random logic circuits, the aforementioned SAT and CI-based approaches are infeasible
for rectification of arithmetic circuits.

**1.1 Problem Description, Objectives, and Contributions**

We address the problem of rectification of buggy finite field arithmetic circuits. Our
problem setup is as follows:

- A specification model (Spec) is given either as a polynomial description $f_{spec}$ over a finite field, or as a golden model of a finite field arithmetic circuit. The finite field considered is the field of $2^k$ elements (denoted by $\mathbb{F}_{2^k}$), where $k$ is the operand-width (bit-vector word length). An implementation (Impl) circuit C is also given.
- Equivalence checking is performed between the *Spec* and the *Impl* circuit *C*, and the presence of a bug is detected. No restrictions on the number, type, or locations of the bugs are assumed.

- We assume that error-diagnosis has been performed, and a subset *X* of the nets of the circuit is identified as *potential rectification locations*, called target nets.

Given the *Spec*, the buggy *Impl* circuit *C*, the set *X* of potential rectifiable locations, our objective is to determine whether or not the buggy circuit can be rectified at *one particular net (location) x<sub>i</sub> ∈ X*. This is called **single-fix rectification** in literature [16]. If a single-fix rectification does exist at net *x<sub>i</sub>* in the buggy circuit, then our subsequent objective is to derive a polynomial function *U(X<sub>PI</sub>)* in terms of the set of primary input variables *X<sub>PI</sub>*. This polynomial needs to be further translated (synthesized) into a logic sub-circuit such that *x<sub>i</sub> = U(X<sub>PI</sub>)* acts as the rectification function for the buggy *Impl* circuit *C* so that this modified *C* matches the specification.

Given the above objective, this article makes the following specific contributions to
solve the debug and rectification problem.

1. We formulate the test for single-fix rectifiability at a net $x_i$ using concepts and techniques from algebraic geometry [12].

- The problem is modeled in polynomial rings of the form $\mathbb{F}_{2^k}[x_1, \dots, x_n]$, where $k$ corresponds to the operand-width and the variables $x_1, \dots, x_n$ are the nets of the circuit.

- The rectification test is formulated using elimination ideals and the Weak Nullstellensatz, and solved using Gröbner basis as a decision procedure.

2. If rectification is feasible at $x_i$, then we compute a rectification function $x_i = U(X_{PI})$.

- We show that the rectification function $U(X_{PI})$ can be determined based on the concept of Craig interpolants in algebraic geometry. While Craig interpolation is a well-studied concept in propositional and first-order logic theories, to the best of our knowledge, it has not been investigated in algebraic geometry.

- We define Craig interpolants in polynomial algebra in finite fields and prove their existence. We also show how to compute such an interpolant using Gröbner bases.

3. The rectification function $U(X_{PI})$ obtained using Craig interpolants is a polynomial in $\mathbb{F}_{2^k}[x_1, \dots, x_n]$. We subsequently show how a logic circuit can be obtained from this polynomial.

4. We use Gröbner basis not only as a decision procedure for the rectification test, but also as a quantification procedure for computing the rectification function. Computation of Gröbner bases exhibits very high complexity. To make our approach scalable, we further show how to exploit the topological structure of the given circuit to improve this computation.

We demonstrate the application of our techniques to rectify finite field arithmetic
circuits with large operand sizes, where conventional SAT-solver based rectification
approaches are infeasible.

The paper is organized as follows. The following section reviews previous work
in automated diagnosis and rectification, and recent applications of Craig interpolants.
Section 3 describes concepts from computer algebra and algebraic geometry. Section 4
describes an equivalence checking framework using the Weak Nullstellensatz over finite
fields. Section 5 presents results that ascertain the single-fix rectifiability of the circuit. Section 6 introduces Craig interpolants in finite fields using Gröbner basis methods, and gives a procedure for obtaining the rectification function through algebraic interpolants. Section 7 addresses improvements to the Gröbner basis computation. Section 8 presents our experimental results and Section 9 concludes the paper.

## 2 Review of Previous Work

Automated diagnosis and rectification of digital circuits has been addressed in [13][18]. The paper [14] presents algorithms for synthesizing Engineering Change Order (ECO) patches. The partial equivalence checking problem has been addressed in [15][19] that checks whether a partial implementation can be extended to a complete design so that it becomes equivalent to a given specification. The partial implementation comprises black-boxes for which some functions $f_i$'s need to be computed. The problem is formulated as Quantified Boolean Formula (QBF) solving: does there exist a function $f_i$, such that for all primary input assignments, the *Impl* circuit is equivalent to the *Spec* circuit. Incremental SAT-solving based approach has been presented in [20] in lieu of solving the QBF problem. This approach has been extended in [21][22] to generate rectification functions when the *Impl* circuit topology is fixed. The use of Craig interpolation as an alternative to quantifier elimination has been presented in [16][23][24] for ECO applications. The single-fix rectification function approach in [23] has been extended in [16] to generate multiple partial-fix functions. Recently, an efficient approach on resource aware ECO patch generation has been presented in [25].

As these approaches are SAT based, they work well for random logic circuits but are not efficient for arithmetic circuits. In contrast, this article presents a word-level formulation for single-fix rectification using algebraic geometry techniques. Computer algebra has been utilized for circuit debugging and rectification in [27],[28],[29]. These approaches rely heavily on the structure of the circuit for debugging, and in general, are incomplete. If the arithmetic circuit contains redundancies, the approach may not identify the buggy gate, nor compute the rectification function. On the other hand, our approach is complete, as it can always compute a single-fix rectification function, if one exists. Although our polynomial algebra based approach is applicable to any circuit in general, it is more efficient and practical for finite field arithmetic circuits.

The concept of Craig interpolants has been extensively investigated in many first order theories for various applications in synthesis and verification. Given the pair $(A, B)$ of two mutually inconsistent formulas (cf. Def. 1.1) and a proof of their unsatisfiability, a procedure called the *interpolation system* constructs the interpolant in linear time and space in the size of the proof [30]. As the abilities of SAT solvers for proof refutation have improved, interpolants have been exploited as abstractions in various problems that can be formulated as unsatisfiable instances, e.g. model checking [30], logic synthesis [31], etc. Their use as abstractions have also been replicated in other (combinations of) theories [32] [33] [34] [35], etc. However, the problem has been insufficiently investigated over polynomial ideals in finite fields from an algebraic geometry perspective. In that regard, the works that come closest to ours are by Gao *et al.* [36] and [37]. While they do not address the interpolation problem per se, they do describe important results
of Nullstellensatz, projections of varieties and quantifier elimination over finite fields
that we utilize to develop the theory and algorithms for our approach. Moreover, prior to
discovering, our approach requires that verification be performed to detect the presence
of a bug. For this purpose, we make use of techniques presented in [38] [7] [8].

We have described the notion of Craig interpolants in finite fields in our work [26]. This article is an extended version of that work where we formally define Craig interpolants in finite fields and prove their existence. Moreover, we describe a procedure for computing an interpolant and prove that the computed interpolant is the smallest. The computation of interpolants uses Gröbner basis based algorithms which have high computational complexity. In contrast to [26], we further propose an efficient approach to compute interpolants based on the given circuit topology.

3 Preliminaries: Notation and Background Results

Let $\mathbb{F}_q$ denote the finite field of $q = 2^k$, $\bar{\mathbb{F}}_q$ be its algebraic closure, and $k$ is the operand width. The field $\mathbb{F}_{2^k}$ is constructed as $\mathbb{F}_{2^k} = \mathbb{F}_2[x] \pmod{P(x)}$, where $\mathbb{F}_2 = \{0,1\}$, and $P(x)$ is a primitive polynomial of degree $k$. Let $\alpha$ be a primitive element of $\mathbb{F}_{2^k}$, so that $P(\alpha) = 0$. Let $R = \mathbb{F}_q[x_1, \dots, x_n]$ be the polynomial ring in $n$ variables $x_1, \dots, x_n$, with coefficients from $\mathbb{F}_q$. A monomial is a power product of variables $x_1^{e_1} \cdot x_2^{e_2} \cdots x_n^{e_n}$, where $e_i \in \mathbb{Z}_{\ge 0}, i \in \{1, \dots, n\}$. A polynomial $f \in R$ is written as a finite sum of terms $f = c_1X_1 + c_2X_2 + \cdots + c_tX_t$, where $c_1, \dots, c_t$ are coefficients and $X_1, \dots, X_t$ are monomials. A monomial order $> (\text{or a term order})$ is imposed on the ring — i.e. a total order and a well-order on all the monomials of $R$ s.t. multiplication with another monomial preserves the order. Then the monomials of all polynomials $f = c_1X_1 + c_2X_2 + \cdots + c_tX_t$ are ordered w.r.t. $>$, such that $X_1 > X_2 > \cdots > X_t$, where $\text{lm}(f) = X_1$, $\text{lt}(f) = c_1X_1$, and $\text{lc}(f) = c_1$ are called the *leading monomial*, *leading term*, and *leading coefficient* of $f$, respectively. In this work, we employ lexicographic (lex) term orders (see Definition 1.4.3 in [12]).

**Polynomial reduction via division:** Let $f, g$ be polynomials. If $\text{lm}(f)$ is divisible by $\text{lm}(g)$, then we say that $f$ is reducible to $r$ modulo $g$, denoted $f \xrightarrow{g} r$, where $r = f - \frac{\text{lt}(f)}{\text{lt}(g)} \cdot g$. This operation forms the core operation of polynomial division algorithms and it has the effect of canceling the leading term of $f$. Similarly, $f$ can be reduced w.r.t. a set of polynomials $F = \{f_1, \dots, f_s\}$ to obtain a remainder $r$. This reduction is denoted as $f \xrightarrow{F} r$, and the remainder $r$ has the property that no term in $r$ is divisible (i.e. cannot be canceled) by the leading term of any polynomial $f_i$ in $F$.

We model the given circuit C by a set of multivariate polynomials $f_1, \dots, f_s \in \mathbb{F}_{2^k}[x_1, \dots, x_n]$; here $x_1, \dots, x_n$ denote the nets (signals) of the circuit. Every Boolean logic gate of C is represented by a polynomial in $\mathbb{F}_2$, as $\mathbb{F}_2 \subset \mathbb{F}_{2^k}$. This is shown below. Note that in $\mathbb{F}_{2^k}$, $-1 = +1$.

$$
\begin{align*}
z &= \neg a \rightarrow z + a + 1 \pmod{2} \\
z &= a \wedge b \rightarrow z + a \cdot b \pmod{2} \\
z &= a \vee b \rightarrow z + a + b + a \cdot b \pmod{2} \\
z &= a \oplus b \rightarrow z + a + b \pmod{2}
\end{align*}
\tag{1}
$$
**Definition 3.1.** (Ideal of polynomials) Given a set of polynomials $F = \{f_1, \dots, f_s\}$ in $\mathbb{F}_q[x_1, \dots, x_n]$, the ideal $J \subseteq R$ generated by $F$ is,

$$J = \langle f_1, \dots, f_s \rangle = \{ \sum_{i=1}^{s} h_i \cdot f_i : h_i \in \mathbb{F}_q[x_1, \dots, x_n] \}.$$

The polynomials $f_1, \dots, f_s$ form the basis or the generators of $J$.

Let $\mathbf{a} = (a_1, \dots, a_n) \in \mathbb{F}_q^n$ be a point in the affine space, and $f$ a polynomial in $R$. If $f(\mathbf{a}) = 0$, we say that $f$ vanishes on $\mathbf{a}$. In verification, we have to analyze the set of all common zeros of the polynomials of $F$ that lie within the field $\mathbb{F}_q$. In other words, we need to analyze solutions to the system of polynomial equations $f_1 = f_2 = \dots = f_s = 0$. This zero set is called the variety. It depends not just on the given set of polynomials but rather on the ideal generated by them. We denote it by $V(J) = V(f_1, \dots, f_s)$, and it is defined as follows:

**Definition 3.2.** (Variety of an ideal) Given a set of polynomials $F = \{f_1, \dots, f_s\}$ in $\mathbb{F}_q[x_1, \dots, x_n]$, their variety

$$V(J) = V(f_1, \dots, f_s) = \{ \mathbf{a} \in \mathbb{F}_q^n : \forall f \in J, f(\mathbf{a}) = 0 \}$$

We denote the complement of a variety, $\mathbb{F}_q^n \setminus V(J)$, by $\overline{V(J)}$.

**The Weak Nullstellensatz:** To ascertain whether $V(J) = \emptyset$, we employ the Weak Nullstellensatz over $\mathbb{F}_q$, for which we use the following notations.

**Definition 3.3.** (Sum and Product of Ideals) Given two ideals $J_1 = \langle f_1, \dots, f_s \rangle, J_2 = \langle h_1, \dots, h_r \rangle$, their sum and product are

$$J_1 + J_2 = \langle f_1, \dots, f_s, h_1, \dots, h_r \rangle \\ J_1 \cdot J_2 = \langle f_i \cdot h_j : 1 \le i \le s, 1 \le j \le r \rangle$$

Ideals and varieties are dual concepts: $V(J_1 + J_2) = V(J_1) \cap V(J_2)$, and $V(J_1 \cdot J_2) = V(J_1) \cup V(J_2)$. Moreover, if $J_1 \subseteq J_2$ then $V(J_1) \supseteq V(J_2)$.

For all elements $\alpha \in \mathbb{F}_q$, $\alpha^q = \alpha$. Therefore, the polynomial $x^q - x$ vanishes everywhere in $\mathbb{F}_q$, and is called the vanishing polynomial of the field. Let $J_0 = \langle x_1^q - x_1, \dots, x_n^q - x_n \rangle$ be the ideal of all vanishing polynomials in $R$. Then the variety of ideal $J_0$ is the entire affine space, i.e. $V(J_0) = \mathbb{F}_q^n$. Moreover, by extending any ideal $J \in R = \mathbb{F}_q[x_1, \dots, x_n]$ by the ideal of all vanishing polynomials in $R$, the variety is restricted to points within $\mathbb{F}_q^n$, i.e. $V(J + J_0) \subset \mathbb{F}_q^n$.

**Theorem 3.1** (The Weak Nullstellensatz over finite fields (from Theorem 3.3 in [37])).
For a finite field $\mathbb{F}_q$ and the ring $R = \mathbb{F}_q[x_1, \dots, x_n]$, let $J = \langle f_1, \dots, f_s \rangle \subseteq R$, and let $J_0 = \langle x_1^q - x_1, \dots, x_n^q - x_n \rangle$ be the ideal of vanishing polynomials. Then $V(J) = \emptyset \iff 1 \in J + J_0$.
To determine whether $V(J) = \emptyset$, we need to test whether or not the unit element 1 is a member of the ideal $J+J_0$. For this ideal membership test, we need to compute a Gröbner basis of $J+J_0$.

**Gröbner basis of ideals:** An ideal may have many different sets of generators: $J = \langle f_1, \dots, f_s \rangle = \dots = \langle g_1, \dots, g_t \rangle$. Given a non-zero ideal $J$, a Gröbner basis (GB) for $J$ is one such set $G = \{g_1, \dots, g_t\}$ that possesses important properties that allow to solve many polynomial decision problems.

**Definition 3.4 (Gröbner basis [12]).** For a monomial ordering $>$, a set of non-zero polynomials $G = \{g_1, g_2, \dots, g_t\}$ contained in an ideal $J$, is called a Gröbner basis of $J$ iff $\forall f \in J, f \neq 0$, there exists $g_i \in \{g_1, \dots, g_t\}$ such that $\text{lm}(g_i)$ divides $\text{lm}(f)$; i.e., $G = GB(J) \Leftrightarrow \forall f \in J: f \neq 0, \exists g_i \in G: \text{lm}(g_i) | \text{lm}(f)$.

Then $J = \langle G \rangle$ holds and so $G = GB(J)$ forms a basis for $J$. Buchberger's algorithm [39] is used to compute a Gröbner basis. The algorithm, shown in Alg. 1, takes as input the set of polynomial $F = \{f_1, \dots, f_s\}$ and computes their Gröbner basis $G = \{g_1, \dots, g_t\}$ such that $J = \langle F \rangle = \langle G \rangle$, where the variety $V(\langle F \rangle) = V(\langle G \rangle) = V(J)$. In the algorithm,

$$Spoly(f_i, f_j) = \frac{L}{\text{lt}(f_i)} \cdot f_i - \frac{L}{\text{lt}(f_j)} \cdot f_j \quad (2)$$

where $L = \text{LCM}(\text{lm}(f_i), \text{lm}(f_j))$.

<table><caption>**Algorithm 1 Buchberger's Algorithm**</caption><tr><td><b>Require:</b></td><td>$F = \{f_1, \dots, f_s\}$</td></tr><tr><td><b>Ensure:</b></td><td>$G = \{g_1, \dots, g_t\}$</td></tr><tr><td>1:</td><td>$G := F$;</td></tr><tr><td>2:</td><td><b>while</b> $G' \neq G$ <b>do</b></td></tr><tr><td>3:</td><td>$G' := G$</td></tr><tr><td>4:</td><td><b>for</b> each pair $\{f_i, f_j\}, i \neq j$ in $G'$ <b>do</b></td></tr><tr><td>5:</td><td>$Spoly(f_i, f_j) \xrightarrow{G'} h$</td></tr><tr><td>6:</td><td><b>if</b> $h \neq 0$ <b>then</b></td></tr><tr><td>7:</td><td>$G := G \cup \{h\}$</td></tr></table>

A GB may contain redundant polynomials, and it can be reduced to eliminate these redundant polynomials from the basis. A reduced GB is a canonical representation of the ideal. Moreover, when $1 \in J$, then $G = \text{reduced\_GB}(J) = \{1\}$. Therefore, to check if $V(J) = \emptyset$, from Thm. 3.1 we compute a reduced GB $G$ of $J+J_0$ and see if $G = \text{GB}(J+J_0) = \{1\}$. If so, the generators of ideal $J$ do not have any common zeros in $\mathbb{F}_q^n$.

**Craig interpolation:** The Weak Nullstellensatz is the polynomial analog of SAT checking. For UNSAT problems, the formal logic and verification communities have explored the notion of abstraction of functions by means of Craig interpolants, which has been applied to circuit rectification [16].
Given the pair $(A, B)$ and their refutation proof, a procedure called the interpolation system constructs the interpolant in linear time and space in the size of the proof [30]. We introduce the notion of Craig interpolants in polynomial algebra over finite fields, based on the results of the Nullstellensatz. We make use of the following definitions and theorems for describing the results on Craig interpolants in finite fields.

**Definition 3.5.** Given an ideal $J \subset R$ and $V(J) \subseteq \mathbb{F}_q^n$, the ideal of polynomials that vanish on $V(J)$ is $I(V(J)) = \{f \in R : \forall \mathbf{a} \in V(J), f(\mathbf{a}) = 0\}$.

If $I_1 \subset I_2$ are ideals then $V(I_1) \supset V(I_2)$, and similarly if $V_1 \subset V_2$ are varieties, then $I(V_1) \supset I(V_2)$.

**Definition 3.6.** For any ideal $J \subset R$, the **radical** of $J$ is defined as $\sqrt{J} = \{f \in R : \exists m \in \mathbb{N} \text{ s.t. } f^m \in J\}$.

When $J = \sqrt{J}$, then $J$ is called a radical ideal. Over algebraically closed fields, the *Strong Nullstellensatz* establishes the correspondence between radical ideals and varieties. Over finite fields, it has a special form.

**Lemma 3.1.** (From [36]) For an arbitrary ideal $J \subset \mathbb{F}_q[x_1, \dots, x_n]$, and $J_0 = \langle x_1^q - x_1, \dots, x_n^q - x_n \rangle$, the ideal $J+J_0$ is radical; i.e. $\sqrt{J+J_0} = J+J_0$.

**Theorem 3.2 (The Strong Nullstellensatz over finite fields (Theorem 3.2 in [36]))**. For any ideal $J \subset \mathbb{F}_q[x_1, \dots, x_n]$, $I(V(J)) = J+J_0$.

**Definition 3.7.** Given an ideal $J \subset \mathbb{F}_q[x_1, \dots, x_n]$, the $l$-th elimination ideal $J_l$ is an ideal in $R$ defined as $J_l = J \cap \mathbb{F}_q[x_{l+1}, \dots, x_n]$.

**Theorem 3.3 (Elimination Theorem (from Theorem 2.3.4 [12]))**. Given an ideal $J \subset R$ and its GB $G$ w.r.t. the lexicographical (lex) order on the variables where $x_1 > x_2 > \dots > x_n$, then for every $0 \le l \le n$ we denote by $G_l$ the GB of $l$-th elimination ideal of $J$ and compute it as:

$$G_l = G \cap \mathbb{F}_q[x_{l+1}, \dots, x_n].$$

$J_l$ is called the $l$-th elimination ideal as it eliminates the first $l$ variables from $J$.

**Example 3.1.** (from [11]) Consider polynomials $f_1: x^2 - y - z - 1$, $f_2: x - y^2 - z - 1$, and $f_3: x - y - z^2 - 1$ and the ideal $J = \langle f_1, f_2, f_3 \rangle \subset \mathbb{C}[x, y, z]$. GB($J$) with lex term order $x > y > z$ equals to $\{g_1: x - y - z^2 - 1, g_2: y^2 - y - z^2 - z, g_3: 2yz^2 - z^4 - z^2, g_4: z^6 - 4z^4 - 4z^3 - z^2\}$. Then, the GB of 2nd elimination ideal of $J$ is $G_2 = GB(J) \cap \mathbb{C}[z] = \{g_4\}$ and GB of 1st elimination ideal is $G_1 = GB(J) \cap \mathbb{C}[y, z] = \{g_2, g_3, g_4\}$.

**Definition 3.8.** Given an ideal $J = \langle f_1, \dots, f_s \rangle \subset R$ and its variety $V(J) \subset \mathbb{F}_q^n$, the $l$-th projection of $V(J)$ denoted as $Pr_l(V(J))$ is the mapping

$$Pr_l(V(J)) : \mathbb{F}_q^n \to \mathbb{F}_q^{n-l}, \quad Pr_l(a_1, \dots, a_n) = (a_{l+1}, \dots, a_n),$$

for every $\mathbf{a} = (a_1, \dots, a_n) \in V(J)$.

In a general setting, the projection of a variety is a subset of the variety of an elimination ideal: $Pr_l(V(J)) \subseteq V(J_l)$. However, operating over finite fields, when the ideals contain the vanishing polynomials, then the above set inclusion turns into an equality.
**Lemma 3.2** (Lemma 3.4 in [36]). Given an ideal $J \subset R$ that contains the vanishing polynomials of the field, then $Pr_I(V(J)) = V(J_I)$, i.e. the $l$-th projection of the variety of ideal $J$ is equal to the variety of its $l$-th elimination ideal.

# 4 Algebraic Miter for Equivalence Checking

Given $f_{spec}$ as the *Spec* polynomial and an *Impl* circuit *C*, we need to construct an *algebraic miter* between $f_{spec}$ and *C*. For equivalence checking, we need to prove that the miter is infeasible. Fig. 1 depicts how a word-level algebraic miter is setup. Suppose that $A = \{a_0, \dots, a_{k-1}\}$ and $Z = \{z_0, \dots, z_{k-1}\}$ denote the $k$-bit primary inputs and outputs of the finite field circuit, respectively. Then $A = \sum_{i=0}^{k-1} a_i \alpha^i$, $Z = \sum_{i=0}^{k-1} z_i \alpha^i$ correspond to polynomials that relate the word-level and bit-level inputs and outputs of *C*. Here $\alpha$ is the primitive element of $\mathbb{F}_{2^k}$. Let $Z_S$ be the word-level output for $f_{spec}$, which computes some polynomial function $\mathcal{F}(A)$ of $A$, so that $f_{spec} : Z_S + \mathcal{F}(A)$. The word-level outputs $Z, Z_S$ are mitered to check if for all inputs, $Z \neq Z_S$ is infeasible.

<figure><img src="image_2.png" /><figcaption>Fig. 1: Word-Level Miter</figcaption></figure>

The logic gates of *C* are modeled as the set of polynomials $F = \{f_1, \dots, f_S\}$ according to Eqn. (1). In finite fields, the disequality $Z \neq Z_S$ can be modeled as a single polynomial $f_m$, called the miter polynomial, where $f_m = t \cdot (Z - Z_S) - 1$, and $t$ is introduced as a free variable. If $Z = Z_S$, then $Z - Z_S = 0$. So $f_m : t \cdot 0 + 1 = 0$ has no solutions (miter is infeasible). Whereas if for some input $A$, $Z \neq Z_S$, then $Z - Z_S \neq 0$. Let $t^{-1} = (Z - Z_S)^{-1} \neq 0$. Then $f_m : t \cdot t^{-1} - 1 = 0$ has a solution as $(t, t^{-1})$ are multiplicative inverses of each other. Thus the miter becomes feasible.

Corresponding to the miter, we construct the ideal $J = \langle f_{spec}, f_1, \dots, f_S, f_m \rangle$. In our formulation, we need to also include the ideal $J_0$ corresponding to the vanishing polynomials in variables $Z, Z_S, A, t$, and $x_i$; here $Z, Z_S, A, t$ are the word-level variables that take values in $\mathbb{F}_{2^k}$, and $x_i$ corresponds to the bit level (Boolean) variables in the miter. In fact, it was shown in [7] that in $J_0$ it is sufficient to include vanishing polynomials for only the primary input bits ($x_i \in X_{PI}$). Therefore, $J_0 = \langle x_i^2 - x_i : x_i \in X_{PI} \rangle$.
In this way, equivalence checking using the algebraic model is solved as follows: Construct an ideal $J = \langle f_{spec}, f_1, \dots, f_s, f_m \rangle$, as described above. Add to it the ideal $J_0 = \langle x_i^2 - x_i : x_i \in X_{PI} \rangle$. Determine if the variety $V(J+J_0) = \emptyset$, i.e. if reduced GB($J+J_0$) = $\{1\}$? If $V(J+J_0) = \emptyset$, the miter is infeasible, and C implements $f_{spec}$. If $V(J+J_0) \neq \emptyset$, the miter is feasible, and there exists a bug in the design.

<figure><img src="image_3.png" /><figcaption>Fig. 2: Correct (a) and buggy (b) 2-bit modulo multiplier circuit implementations</figcaption></figure>

**Example 4.1.** Consider a modulo multiplier with output Z and inputs A, B. The Spec polynomial is given as $f_{spec} : Z+A \cdot B \pmod{P(X)}$, where P(X) is a primitive polynomial of the field. An implementation of such a multiplier with operand (Z, A, B) bit-width = 2 is shown in Fig. 2(a).

Now let's say that the designer has introduced a bug, and the XOR gate with output net $r_0$ has been replaced with an AND gate in the actual implementation in the circuit of Fig. 2(b). The polynomials for the gates of the correct circuit implementation are,

$$f_1 : c_0 + a_0 \cdot b_0, \quad f_2 : c_1 + a_0 \cdot b_1, \quad f_3 : c_2 + a_1 \cdot b_0, \quad f_4 : c_3 + a_1 \cdot b_1, \\ f_5 : r_0 + c_1 + c_2, \quad f_6 : z_0 + c_0 + c_3, \quad f_7 : z_1 + r_0 + c_3,$$

whereas for the buggy implementation, the polynomial $f_5$ is $f_5' : r_0 + c_1 c_2$. The problem is modeled over $\mathbb{F}_4$ and let $\alpha$ be a primitive element of $\mathbb{F}_4$. The word-level polynomials are $f_8 : Z + z_0 + z_1 \alpha$, $f_9 : A + a_0 + a_1 \alpha$, and $f_{10} : B + b_0 + b_1 \alpha$. The specification polynomial is $f_{spec} : Z_s + AB$. We create a miter polynomial against this specification as $f_m : t(Z - Z_s) - 1$.

To perform equivalence checking of the correct implementation and the specification polynomial, we construct ideal $J = \langle f_{spec}, f_1, \dots, f_5, \dots, f_{10}, f_m \rangle$. Computing GB of $J+J_0$ ($J_0$ is the ideal of vanishing polynomials) results in $\{1\}$, implying the circuit in Fig. 2(a) is equivalent to the specification. However, computing GB of the ideal $J' + J_0$ where $J' = \langle f_{spec}, f_1, \dots, f_5', \dots, f_{10}, f_m \rangle$ results in a set of polynomials $G = \{g_1, \dots, g_t\} \neq \{1\}$, implying the presence of a bug(s) in the design.

# 5 Formulating the Rectification Check

Equivalence checking is performed between the *Spec* and *Impl* circuit C, and it reveals the presence of a bug in the design. Post-verification, we assume that error diagnosis has
been performed, and a set of nets X has been identified as potential single-fix rectifiable locations. While the nets in X might be target nets for single-fix, the circuit may or may not be rectifiable at any $x_i \in X$. We have to first ascertain that the circuit is indeed single-fix rectifiable at some $x_i \in X$, and subsequently compute a rectification function $U(X_{PI})$, so that $x_i = U(X_{PI})$ rectifies the circuit at that net.

## 5.1 Single Fix Rectification

Using the Weak Nullstellensatz (Theorem 3.1), we formulate the test for rectifiability of C at a net $x_i$ in the circuit. For this purpose, we state and prove the following result, which is utilized later.

**Proposition 5.1.** Given two ideals $J_1$ and $J_2$ over some finite field such that $V(J_1) \cap V(J_2) = \emptyset$, there exists a polynomial $U$ which satisfies $V(J_1) \subseteq V(U) \subseteq \bar{V}(J_2)$.

*Proof.* Over finite fields $\mathbb{F}_q$, $V(J_1)$ and $V(J_2)$ are finite sets of points. Every finite set of points is a variety of some ideal. Therefore, given $V(J_1) \cap V(J_2) = \emptyset$, there exists a set of points (a variety) which contains $V(J_1)$, and which does not intersect with $V(J_2)$. Let this variety be denoted by $V(J_I)$, where $J_I$ is the corresponding ideal. Then $V(J_1) \subseteq V(J_I) \subseteq \bar{V}(J_2)$. In addition, we can construct a polynomial $U$ that vanishes exactly on the points in $V(J_I)$ by means of the Lagrange's interpolation formula. $\square$

We now present the result that ascertains the circuit's rectifiability at a target net. Let the net $x_i \in X$ (i.e. $i^{th}$ gate) be the rectification target, and a possible rectification function be $x_i = U(X_{PI})$. Then the $i^{th}$ gate is represented by a polynomial $f_i : x_i + U(X_{PI}) \to U(X_{PI})$. Consider the ideal $J$ corresponding to the algebraic miter – the polynomials $f_1, \dots, f_i, \dots, f_s$ representing the gates of the circuit, the specification polynomial $f_{spec}$, and the miter polynomial $f_m$:

$$J = \langle f_{spec}, f_1, \dots, f_i : x_i + U(X_{PI}), \dots, f_s, f_m \rangle.$$

The following theorem checks whether the circuit is indeed single-fix rectifiable at the net $x_i$.

**Theorem 5.1.** Construct two ideals:

- $J_L = \langle f_{spec}, f_1, \dots, f_i : x_i + 1, \dots, f_s, f_m \rangle$ where $f_i : x_i + U(X_{PI})$ in $J$ is replaced with $f_i : x_i + 1$.

- $J_H = \langle f_{spec}, f_1, \dots, f_i : x_i, \dots, f_s, f_m \rangle$ where $f_i : x_i + U(X_{PI})$ in $J$ is replaced with $f_i : x_i$.

Compute $E_L = (J_L + J_0) \cap \mathbb{F}_{2^k}[X_{PI}]$ and $E_H = (J_H + J_0) \cap \mathbb{F}_{2^k}[X_{PI}]$ to be the respective elimination ideals, where all the non-primary input variables have been eliminated. Then the circuit can be single-fix rectified at net $x_i$ with the polynomial function $f_i : x_i + U(X_{PI})$ to implement the specification iff $1 \in E_L + E_H$.
*Proof.* We will first prove the *if* case of the theorem. Assume $1 \in E_L + E_H$, or equivalently $V_{X_{PI}}(E_L) \cap V_{X_{PI}}(E_H) = \emptyset$. The subscript $X_{PI}$ in $V_{X_{PI}}$ denotes that the variety is being considered over $X_{PI}$ variables, as the non-primary inputs have been eliminated from $E_L$ and $E_H$. Using Proposition 5.1, we can find a polynomial $U(X_{PI})$ such that,

$$V_{X_{PI}}(E_L) \subseteq V_{X_{PI}}(U(X_{PI})) \subseteq \overline{V_{X_{PI}}(E_H)}. \qquad (3)$$

Note, however, that since $V_{X_{PI}}(E_L)$, $V_{X_{PI}}(E_H)$ are considered over only primary input bits, they contain points from $\mathbb{F}_2^{|X_{PI}|}$. Therefore, there exists a polynomial $U(X_{PI})$ as in Eqn. (3) with coefficients only in $\mathbb{F}_2$.

Let us consider a point $\mathbf{p}$ in $V(J)$. Point $\mathbf{p}$ is an assignment to every variable in $J$ such that all the generators of $J$ are satisfied. We denote by $\mathbf{a}$, the projection of $\mathbf{p}$ on the primary inputs (i.e. the primary input assignments under $\mathbf{p}$). There are only two possibilities for $U(X_{PI})$,

1. $U(\mathbf{a}) = 1$, or in other words $\mathbf{a} \notin V_{X_{PI}}(U(X_{PI}))$. It also implies that the value of $x_i$ under $\mathbf{p}$ must be 1 because $x_i + U(X_{PI}) = 0$ needs to be satisfied. Since the generator $f_i$ of $J_L$ also forces $x_i$ to be 1 and all other generators are exactly the same as those of $J$, $\mathbf{p}$ is also a point in $V(J_L)$. Moreover, $E_L$ is the elimination ideal of $J_L$, and therefore, $\mathbf{a} \in V_{X_{PI}}(E_L)$. But this a contradiction to our assumption that $V_{X_{PI}}(E_L) \subseteq V_{X_{PI}}(U(X_{PI}))$ and such a point $\mathbf{a}$ (and $\mathbf{p}$) does not exist.

2. $U(\mathbf{a}) = 0$, or in other words $\mathbf{a} \in V_{X_{PI}}(U(X_{PI}))$. Using similar argument as the previous case, we can show that $\mathbf{a} \in V_{X_{PI}}(E_H)$. This is again a contradiction to our assumption $V_{X_{PI}}(U(X_{PI})) \subseteq \overline{V_{X_{PI}}(E_H)}$.

In conclusion, there exists no point in $V(J)$ (or the miter is infeasible) when $U(X_{PI})$ satisfies Eqn. 3, and therefore, circuit can be rectified at $x_i$.

Now we will prove the *only if* direction of the proof. We show that if $1 \notin E_L + E_H$, then there exists no polynomial $U(X_{PI})$ that can rectify the circuit. If $1 \notin E_L + E_H$, then $E_L$ and $E_H$ have a common zero. Let $\mathbf{a}$ be a point in $V_{X_{PI}}(E_L)$ and $V_{X_{PI}}(E_H)$. This point can be extended to some points $\mathbf{p}'$ and $\mathbf{p}''$ in $V(J_L)$ and $V(J_H)$, respectively. Notice that in point $\mathbf{p}'$ the value of $x_i$ will be 1, and in $\mathbf{p}''$ $x_i$ will be 0. Any polynomial $U(X_{PI})$ will either evaluate to 0 or 1 for the assignment $\mathbf{a}$ to the primary inputs. If it evaluates to 1, then we can say that $\mathbf{p}'$ is in $V(J)$ as $f_i$ in $J$ forces $x_i = 1$ and all other generators of $J$ and $J_L$ are same. This implies that $f_m(\mathbf{p}') = 0$ ($f_m$: miter polynomial is feasible) and this choice of $U(X_{PI})$ will not rectify the circuit. If $U(X_{PI})$ evaluates to 0, then $\mathbf{p}''$ is a point in $V(J)$.

Therefore, no choice of $U(X_{PI})$ can rectify the circuit if $1 \notin E_L + E_H$. $\square$

**Example 5.1.** Consider the buggy modulo multiplier circuit of Fig. 2(b) (reproduced in Fig. 3), where the gate output $r_0$ should have been the output of an XOR gate, but an AND gate is incorrectly implemented. We apply Thm. 5.1 to check for single-fix rectifiability at $r_0$. The polynomials for the gates of the correct circuit implementation are,

$$f_1 : c_0 + a_0 \cdot b_0, \quad f_2 : c_1 + a_0 \cdot b_1, \quad f_3 : c_2 + a_1 \cdot b_0, \quad f_4 : c_3 + a_1 \cdot b_1,$$

$$f_5 : r_0 + c_1 + c_2, \quad f_6 : z_0 + c_0 + c_3, \quad f_7 : z_1 + r_0 + c_3$$
<figure><img src="image_4.png" /><figcaption>Fig. 3: A buggy 2-bit modulo multiplier circuit</figcaption></figure>

The problem is modeled over $\mathbb{F}_4$ and let $\alpha$ be a primitive element of $\mathbb{F}_4$. The word-level polynomials are $f_8: Z + z_0 + z_1\alpha$, $f_9: A + a_0 + a_1\alpha$, and $f_{10}: B + b_0 + b_1\alpha$. The specification polynomial is $f_{spec}: Z_s + AB$. We create a miter polynomial against this specification as $f_m: t(Z - Z_s) - 1$.

The ideals $J_L$ and $J_H$ are constructed as:

$$J_L = \langle f_{spec}, f_1, \dots, f_4, r_0 + 1, f_6, \dots, f_{10}, f_m \rangle$$

$$J_H = \langle f_{spec}, f_1, \dots, f_4, r_0, f_6, \dots, f_{10}, f_m \rangle$$

The ideal $J_0$ is:

$$J_0 = \langle b_1^2 - b_1, b_0^2 - b_0, a_1^2 - a_1, a_0^2 - a_0 \rangle,$$

and the corresponding ideals $E_L$ and $E_H$ are computed to be:

$$E_L = \langle a_0 b_1 + a_1 b_0, a_1 b_0 b_1 + a_1 b_0, a_0 a_1 b_0 + a_1 b_0 \rangle$$

$$E_H = \langle b_0 b_1 + b_0 + b_1 + 1, a_1 b_1 + a_1 + b_1 + 1, a_0 b_1 + a_1 b_0 + 1, a_0 b_0 + a_0 + b_0 + 1, a_0 a_1 + a_0 + a_1 + 1 \rangle$$

Computing a Gröbner basis $G$ of $E_L + E_H$ results in $G = \{1\}$. Therefore, we can rectify this circuit at $r_0$.

On the other hand, if we apply the rectification theorem at net $c_2$, the respective ideals $E_L$ and $E_H$ are as follows,

$$E_L = \langle a_0^2 + a_0, a_1^2 + a_1, b_0^2 + b_0, b_1^2 + b_1, a_1 b_0 + b_0, a_0 b_1 b_0 + a_0 b_1 + a_0 b_0 + a_0, a_0 a_1 + a_0 \rangle$$

$$E_H = \langle a_0^2 + a_0, b_0^2 + b_0, b_1^2 + b_1, b_1 b_0 + b_1 + b_0 + 1, a_1 + 1, a_0 b_0 + a_0 + b_0 + 1 \rangle$$

When we compute $G = GB(E_L + E_H)$, we obtain $G \neq \{1\}$ indicating that single-fix rectification is not possible at net $c_2$, for the given bug.

# 6 Craig Interpolants in Finite Fields

Once it is ascertained that a net $x_i$ admits single-fix rectification, the subsequent task is to compute a rectification polynomial function $x_i = U(X_{PI})$ in terms of the primary
inputs of the circuit. In this section, we describe how such a rectification polynomial function can be computed. For this purpose, we introduce the concept of Craig interpolants using algebraic geometry in finite fields.

We describe the setup for Craig interpolation in the ring $R = \mathbb{F}_q[x_1, \dots, x_n]$. Partition the variables $\{x_1, \dots, x_n\}$ into disjoint subsets $A, B, C$. We are given two ideals $J_A \subset \mathbb{F}_q[A, C]$, $J_B \subset \mathbb{F}_q[B, C]$ such that the C-variables are common to the generators of both $J_A, J_B$. From here on, we will assume that all ideals include the corresponding vanishing polynomials. For example, generators of $J_A$ include $A^q - A, C^q - C$, where $A^q - A = \{x_i^q - x_i : x_i \in A\}$, and so on. Then these ideals become radicals and we can apply Lemmas 3.1 and 3.2. We use $V_{A,C}(J_A)$ to denote the variety of $J_A$ over the $\mathbb{F}_q$-space spanned by $A$ and $C$ variables, i.e. $V_{A,C}(J_A) \subset \mathbb{F}_q^A \times \mathbb{F}_q^C$. Similarly, $V_{B,C}(J_B) \subset \mathbb{F}_q^B \times \mathbb{F}_q^C$.

Now let $J = J_A + J_B \subseteq \mathbb{F}_q[A, B, C]$, and suppose that it is found by application of the Weak Nullstellensatz (Thm. 3.1) that $V_{A,B,C}(J) = \emptyset$. When we compare the varieties of $J_A$ and $J_B$, then we can consider the varieties in $\mathbb{F}_q^A \times \mathbb{F}_q^B \times \mathbb{F}_q^C$, as $V_{A,B,C}(J_A) = V_{A,C}(J_A) \times \mathbb{F}_q^B \subset \mathbb{F}_q^A \times \mathbb{F}_q^B \times \mathbb{F}_q^C$. With this setup, we define the interpolants as follows.

**Definition 6.1 (Interpolants in finite fields).** Given two ideals $J_A \subset \mathbb{F}_q[A, C]$ and $J_B \subset \mathbb{F}_q[B, C]$ where $A, B, C$ denote the three disjoint sets of variables such that $V_{A,B,C}(J_A) \cap V_{A,B,C}(J_B) = \emptyset$. Then there exists an ideal $J_I$ satisfying the following properties:

$$1. V_{A,B,C}(J_I) \supseteq V_{A,B,C}(J_A)$$

$$2. V_{A,B,C}(J_I) \cap V_{A,B,C}(J_B) = \emptyset$$

$$3. \text{Generators of } J_I \text{ contain only the C-variables; or } J_I \subseteq \mathbb{F}_q[C].$$

We call $V_{A,B,C}(J_I)$ the **interpolant** in finite fields of the pair $(V_{A,B,C}(J_A), V_{A,B,C}(J_B))$, and the corresponding ideal $J_I$ the **ideal-interpolant**.

As the generators of $J_I$ contain only the C-variables, the interpolant $V_{A,B,C}(J_I)$ is of the form $V_{A,B,C}(J_I) = \mathbb{F}_q^A \times \mathbb{F}_q^B \times V_C(J_I)$. Therefore, the subscripts A, B for the interpolant $V_{A,B,C}(J_I)$ may be dropped for the ease of readability.

**Example 6.1.** Consider the ring $R = \mathbb{F}_2[a, b, c, d, e]$, partition the variables as $A = \{a\}, B = \{e\}, C = \{b, c, d\}$. Let ideals

$$J_A = \langle ab, bd, bc + c, cd, bd + b + d + 1 \rangle + J_{0,A,C}$$

$$J_B = \langle b, d, ec + e + c + 1, ec \rangle + J_{0,B,C}$$

where $J_{0,A,C}$ and $J_{0,B,C}$ are the corresponding ideals of vanishing polynomials. Then,

$$V_{A,B,C}(J_A) = \mathbb{F}_q^B \times V_{A,C}(J_A) = \\ (abcde) : \{01000,00010,01100,10010,01001,00011,01101,10011\}$$

$$V_{A,B,C}(J_B) = \mathbb{F}_q^A \times V_{B,C}(J_B) = \\ (abcde) : \{00001,00100,10001,10100\}$$

Ideals $J_A, J_B$ have no common zeros as $V_{A,B,C}(J_A) \cap V_{A,B,C}(J_B) = \emptyset$. The pair $(J_A, J_B)$ admits a total of 8 interpolants:
$$
1. V(J_S) = (bcd) : \{001, 100, 110\} \\
J_S = \langle cd, b+d+1 \rangle
$$

$$
2. V_C(J_1) = (bcd) : \{001, 100, 110, 101\} \\
J_1 = \langle cd, bd + b + d + 1, bc + cd + c \rangle
$$

3. $V_C(J_2) = (bcd) : \{001, 100, 110, 011\}$
$J_2 = \langle b+d+1 \rangle$

4. $V_C(J_3) = (bcd) : \{001, 100, 110, 111\}$
$J_3 = \langle b + cd + d + 1 \rangle$

5. $V_C(J_4) = (bcd) : \{001, 100, 110, 011, 111\}$
$J_4 = \langle bd+b+d+1,bc+b+cd+c+d+1 \rangle$

6. $V_C(J_5) = (bcd) : \{001, 100, 110, 101, 111\}$
$J_5 = \langle bc+c,bd+b+d+1 \rangle$

7. $V_C(J_6) = (bcd) : \{001, 100, 110, 101, 011\}$
$J_6 = \langle bd+b+d+1,bc+cd+c \rangle$

8. $V_C(J_L) = (bcd) : \{001, 011, 100, 101, 110, 111\}$
$J_L = \langle bd + b + d + 1 \rangle$.

<figure><img src="image_5.png" /><figcaption>Fig. 4: The Interpolant lattice
for Example 6.1</figcaption></figure>

It is easy to check that all $V(J_I)$ satisfy the 3 conditions of Def. 6.1. Note also that $V(J_S)$ is the smallest interpolant, contained in every other interpolant. Likewise, $V(J_L)$ contains all other interpolants and it is the largest. The other containment relationships are shown in the corresponding interpolant lattice in Fig. 4; $V_C(J_1) \subset V_C(J_5)$, $V_C(J_1) \subset V_C(J_6)$, etc.

**Theorem 6.1.** (Existence of Craig Interpolants) An ideal-interpolant $J_I$, and correspondingly the interpolant $V_{A,B,C}(J_I)$, as given in Def. 6.1, always exists.

*Proof.* Consider the elimination ideal $J_I = J_A \cap \mathbb{F}_q[C]$. We show $J_I$ satisfies the three conditions for the interpolant.

**Condition 1:** $V_{A,B,C}(J_I) \supseteq V_{A,B,C}(J_A)$. This condition is trivially satisfied due to construction of elimination ideals. As $J_I \subseteq J_A$, $V_{A,B,C}(J_I) \supseteq V_{A,B,C}(J_A)$.

Condition 2: $V_{A,B,C}(J_I) \cap V_{A,B,C}(J_B) = \emptyset$. This condition can be equivalently stated as $V_{B,C}(J_I) \cap V_{B,C}(J_B) = \emptyset$ as neither $J_I$ nor $J_B$ contain any variables from the set $A$. We prove this condition by contradiction. Let's assume that there exists a common point $(\mathbf{b}, \mathbf{c})$ in $V_{B,C}(J_I)$ and $V_{B,C}(J_B)$. We know that the projection of the variety $Pr_A(V_{A,C}(J_A))$ is equal to the variety of the elimination ideal $V_C(J_I)$, where $J_I = J_A \cap \mathbb{F}_q[C]$, due to Lemma 3.2. Therefore, the point $(\mathbf{c})$ in the variety of $J_I$ can be extended to a point $(\mathbf{a}, \mathbf{c})$ in the variety of $J_A$. This implies that the ideals $J_A$ and $J_B$ vanish at $(\mathbf{a}, \mathbf{b}, \mathbf{c})$. This is a contradiction to our initial assumption that the intersection of the varieties of $J_A$ and $J_B$ is empty. Thus $J_I, J_B$ have no common zeros.

**Condition 3:** The generators of $J_I$ contain only the $C$-variables. This condition is trivially satisfied as $J_I$ is the elimination ideal obtained by eliminating $A$-variables in $J_A$. $\square$

<figure><img src="image_6.png" /></figure>

The above theorem not only proves the existence of an interpolant, but also gives a procedure to construct its ideal: $J_I = J_A \cap \mathbb{F}_q[C]$. In other words, compute a reduced Gröbner basis $G$ of $J_A$ w.r.t. the elimination order $A > B > C$ and take $G_I = G \cap \mathbb{F}_q[C]$. Then $G_I$ gives the generators for the ideal-interpolant $J_I$.
**Example 6.2.** The elimination ideal $J_I$ computed for $J_A$ from Example 6.1 is $J_I = J_S = \langle cd, b+d+1 \rangle$ with variety $V_C(J_I) = (bcd) : \{001, 100, 110\}$. This variety over the variable set A and C is $V_{A,C}(J_I) = (abcd) : \{0001, 0100, 0110, 1001, 1100, 1110\}$, and it contains $V_{A,C}(J_A)$. Moreover, $V_{A,B,C}(J_I)$ also has an empty intersection with $V_{A,B,C}(J_B)$.

**Theorem 6.2.** (Smallest interpolant) The interpolant $V_{A,B,C}(J_S)$ corresponding to the ideal $J_S = J_A \cap \mathbb{F}_q[C]$ is the smallest interpolant.

*Proof.* Let $J_I \subseteq \mathbb{F}_q[C]$ be any another ideal-interpolant $\neq J_S$. We show that $V_C(J_S) \subseteq V_C(J_I)$. For $V_C(J_I)$ to be an interpolant it must satisfy

$$V_{A,B,C}(J_A) \subseteq V_{A,B,C}(J_I)$$

which, due to Theorem 3.2, is equivalent to

$$I(V_{A,B,C}(J_A)) \supseteq I(V_{A,B,C}(J_I)) \implies J_A \supseteq J_I$$

As the generators of $J_I$ only contain polynomials in C-variables, this relation also holds for the following

$$J_A \cap \mathbb{F}_q[C] \supseteq J_I \implies J_S \supseteq J_I \implies V_C(J_S) \subseteq V_C(J_I).$$

□

## 6.1 Computing a Rectification Function from Craig Interpolants

Back to our formulation of single-fix rectification, from Thm. 5.1 we have $1 \in E_L + E_H$ or $V(E_L) \cap V(E_H) = \emptyset$. Therefore, we can consider the pair $(E_L, E_H)$ for Craig interpolation. In other words, based on the notation from Def. 6.1, $J_A = E_L$ and $J_B = E_H$. Moreover, $E_L$ and $E_H$ are elimination ideals containing only $X_{PI}$ variables. As a result, the partitioned set of variables for Craig interpolation A, B, and C all correspond to primary inputs. Furthermore, we want to compute an ideal $J_I$ in $X_{PI}$ such that $V_{X_{PI}}(E_L) \subseteq V_{X_{PI}}(J_I)$ and $V_{X_{PI}}(J_I) \cap V_{X_{PI}}(E_H) = \emptyset$. The smallest ideal-interpolant $J_I = E_L \cap \mathbb{F}_{2k}[X_{PI}] = E_L$ itself. Therefore, we use $E_L$ to compute the correction function $U(X_{PI})$.

**Obtaining $U(X_{PI})$ from $E_L$:** In finite fields, given an ideal $J$, it always possible to find a polynomial $U$ such that $V(U) = V(J)$. The reason is that every ideal in a finite field has a finite variety, and a polynomial with those points as its roots can always be constructed using the Lagrangian interpolation formula. We construct the rectification polynomial $U$ from the ideal-interpolant $E_L$ as shown below, such that $V(E_L) = V(U)$.

Let the generators of $E_L$ be denoted by $g_1, \dots, g_t$. We can compute $U$ as,

$$U = (1 + g_1)(1 + g_2) \cdots (1 + g_t) + 1 \quad (4)$$

It is easy to assert that $V(U) = V(E_L)$. Consider a point $\mathbf{a}$ in $V(E_L)$. As all of $g_1, \dots, g_t$ vanish (= 0) at $\mathbf{a}$,

$$\begin{aligned} U(\mathbf{a}) &= (1 + g_1(\mathbf{a}))(1 + g_2(\mathbf{a})) \cdots (1 + g_t(\mathbf{a})) + 1 \\ &= (1 + 0)(1 + 0) \cdots (1 + 0) + 1 = 0 \end{aligned}$$
Conversely, for a point $\mathbf{a}' \notin V(E_L)$, at least one of $g_1, \dots, g_t$ will evaluate to 1. Without loss of generality, if $g_1$ evaluates to 1 at $\mathbf{a}'$, then $U = (1+1)(1+0)\cdots(1+0)+1 \neq 0$.

Using Eqn. (4), a recursive procedure is derived to compute $U$, and it is depicted in Algorithm 2. At every recursive step, we also reduce the intermediate results by (mod $J_0$) (line 7) so as to avoid terms of high degree. In this fashion, from the ideal-interpolant $E_L$, we compute the single-fix rectification polynomial function $U(X_{PI})$, and synthesize a sub-circuit at net $x_i$ such that $x_i = U(X_{PI})$ rectifies the circuit.

<caption>**Algorithm 2** Compute $U$ from $J$ such that $V(U) = V(J)$</caption>

1: $U = \text{compute}_U(J, J_0) + 1$
2: **procedure** $\text{compute}_U(J, J_0)$ $l*J = \langle g_1, \dots, g_l \rangle^l$
3: &nbsp;&nbsp;&nbsp;&nbsp;**if** $\text{size}(J) = 1$ **then**
4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** $(1 + J[1])$
5: &nbsp;&nbsp;&nbsp;&nbsp;**subset** $J = \{J[1], J[2], \dots, J[\text{size}(J) - 1]\}$
6: &nbsp;&nbsp;&nbsp;&nbsp;**poly** $S_1 = \text{compute}_U(\text{subset}J, J_0)$
7: &nbsp;&nbsp;&nbsp;&nbsp;**Perform** $S_1 \cdot J[\text{size}(J)] \xrightarrow{J_0} S_2$
8: &nbsp;&nbsp;&nbsp;&nbsp;**return** $S_1 + S_2$

**Example 6.3.** *Example 5.1 showed that the buggy circuit of Fig. 3 can be rectified at net $r_0$. This rectification check required the computation of the (Gröbner basis of) ideal $E_L$. Using Alg. 2, we compute $U(X_{PI})$ from $E_L$ to be $a_0b_1 + a_1b_0$, and the rectification polynomial as $r_0 + a_0b_1 + a_1b_0$. This can be synthesized into a sub-circuit as $r_0 = (a_0 \wedge b_1) \oplus (a_1 \wedge b_0)$, by replacing the modulo 2 product and sum in the polynomial with the Boolean AND and XOR operators, respectively.*

# 7 Efficient Gröbner basis computations for $E_L$ and $E_H$

The proposed rectification approach requires the computation of (generators of) elimination ideals $E_L$ and $E_H$. This is achieved by computing a Gröbner basis each for $GB(J_L + J_0) \cap \mathbb{F}_{2^k}[X_{PI}]$ and $GB(J_H + J_0) \cap \mathbb{F}_{2^k}[X_{PI}]$, respectively. The rectification polynomial function $x_i = U(X_{PI})$ is subsequently derived from the generators of $E_L$. As the generators of $J_L$ and $J_H$ comprise polynomials derived from the entire circuit, these GB-computations become infeasible for larger circuits due to its high complexity. In [37], it was shown that the time and space complexity of computing $GB(J + J_0)$ over $\mathbb{F}_q[x_1, \dots, x_n]$ is bounded by $q^{O(n)}$. In the context of our work, as $q = 2^k$ where $k$ is the operand-width, and $n$ the number of variables (nets) in the miter, we have to overcome this complexity to make our approach practical for large circuits.

Prior work [8] has shown that the GB-computation can be significantly improved when the polynomials are derived from circuits. By analyzing the topology of the given circuit, a specialized term order can be derived that can significantly reduce the number of *Spoly* computations in the GB-algorithm. We present a similar approach to improve the GB-computation for ideals $E_L, E_H$.
**Lemma 7.1 (Product Criterion [40]).** For two polynomials $f_i, f_j$ in any polynomial ring $R$, if the equality $lm(f_i) \cdot lm(f_j) = LCM(lm(f_i),lm(f_j))$ holds, i.e. if $lm(f_i)$ and $lm(f_j)$ are relatively prime, then $Spoly(f_i, f_j) \xrightarrow{G} 0$.

Buchberger's algorithm therefore does not pair those polynomials $f_i, f_j$ (Alg. 1, line 4) whose leading monomials are relatively prime, as they do not produce any new information in the basis. Moreover, based on the above criterion, when the leading monomials of all polynomials in the basis $F = \{f_1, \dots, f_s\}$ are relatively prime, then all $Spoly(f_i, f_j) \xrightarrow{G} 0$. As no new polynomials are generated in Buchberger's algorithm, $F$ already constitutes a Gröbner basis ($F = GB(J)$). For a combinational circuit $C$, a specialized term order $>$ can always be derived by analyzing the circuit topology which ensures such a property [4] [7]:

**Proposition 7.1 (From [7])**. Let $C$ be an arbitrary combinational circuit. Let $\{x_1, \dots, x_n\}$ denote the set of all variables (signals) in $C$. Starting from the primary outputs, perform a reverse topological traversal of the circuit and order the variables such that $x_i > x_j$ if $x_i$ appears earlier in the reverse topological order. Impose a lex term order $>$ to represent each gate as a polynomial $f_i$, s.t. $f_i = x_i + tail(f_i)$. Then the set of all polynomials $\{f_1, \dots, f_s\}$ forms a Gröbner basis $G$, as $lt(f_i) = x_i$ and $lt(f_j) = x_j$ for $i \neq j$ are relatively prime. This term order $>$ is called the **Reverse Topological Term Order (RTTO)**.

RTTO ensures that the set of all polynomials $\{f_1, \dots, f_s\}$ of the given circuit $C$ have relatively prime leading terms. However, the model of the algebraic miter (Fig. 1, with the *Spec* and the miter polynomial, in addition to the given circuit) is such that under RTTO $>$, not all polynomials have relatively prime leading terms. However, we show that imposition of RTTO on the miter still significantly reduces the amount of computation required for Gröbner bases. We demonstrate the technique on the GB computation for the ideal $J_L + J_0$ (analogously also for $J_H + J_0$), corresponding to the miter, as per Thm. 5.1.

Given the word-level miter of Fig. 1, impose a lexicographic (lex) monomial order on the ring $R$, with the following variable order:

$$ t > Z > Z_s > A > \text{nets of } C \text{ in RTTO order} > \text{Primary input variables} \quad (5) $$

Here $t$ is the free variable used in the miter polynomial, and $Z, Z_s$ are the word-level outputs of *Impl* and *Spec*, respectively, and $A$ is the word-level input. Corresponding to the circuit in Fig. 3 (Example 5.1), we use a lex term order with variable order:

$$ t > Z > Z_s > A > B > z_1 > z_0 > r_0 > c_0 > c_1 > c_2 > c_3 > b_1 > b_0 > a_1 > a_0 \quad (6) $$

The polynomials $\{f_1, \dots, f_{10}, f_{spec}, f_m\}$ in Example 5.1 are already written according to the term order of Eqn. (6). Note also that the leading terms of the generators of the ideal $J_L$ are the same as the leading terms of polynomials in $\{f_1, \dots, f_{10}, f_{spec}, f_m\}$. From among these, the only pair of polynomials that do not have relatively prime leading terms are $f_8$ and $f_m$. This condition also holds when considering the ideal $J_L + J_0$ (instead of only $J_L$) as $J_0$ is composed of only bit-level primary input variables.
In general, modeling an algebraic miter with RTTO > will ensure that we have *exactly one pair of polynomials with leading monomials that are not relatively prime.* This pair includes: i) the miter polynomial $f_m : tZ - tZ_s - 1$, with $lm(f_m) = tZ$; and ii) the polynomial (hereafter denoted by $f_o$) that relates the word-level and bit-level variables of the circuit, $f_o : Z + z_0 + z_1\alpha + \cdots + z_{k-1}\alpha^{k-1}$, with $lm(f_o) = Z$. Therefore, in the first iteration of Alg. 1 for computing $GB(J_L + J_0)$, the only critical pair to compute is $Spoly(f_m, f_o)$, as all other pairs reduce to 0, due to Lemma 7.1. Moreover, computing $Spoly(f_m, f_o)$ results in $Spoly(f_m, f_o) = t(Z_s + z_0 + \cdots + z_{k-1}\alpha^{k-1}) + 1$. Once again, RTTO > ensures the following:

**Lemma 7.2.** *Spoly*($f_m, f_o$) $\xrightarrow{J_L+J_0}+_+$ $h = t \cdot r + 1$, where $r$ is a polynomial in bit-level primary input variables.

*Proof.* Consider the polynomial reduction of $Spoly(f_m, f_o)$ $\xrightarrow{J_L+J_0}+_+$ $h$:

$$t(Z_s + z_0 + \cdots + z_{k-1}\alpha^{k-1}) + 1 \xrightarrow{f_{spec}} +$$

where $f_{spec} = Z_s + \mathcal{F}(A)$. The remainder for this reduction will be

$$t(\mathcal{F}(A) + z_0 + \cdots + z_{k-1}\alpha^{k-1}) + 1,$$

where $\mathcal{F}(A)$ is the polynomial specification in word-level input variable(s). This remainder is then reduced by the polynomial relating the word-level and bit-level primary input variables, i.e. by $A + a_0 + \cdots + a_{k-1}\alpha^{k-1}$. The subsequent remainder is

$$t(\mathcal{F}(A) + z_0 + \cdots + z_{k-1}\alpha^{k-1}) + 1 \xrightarrow{A+a_0+\cdots+a_{k-1}\alpha^{k-1}}+_+ \\ t(z_0 + \cdots + z_{k-1}\alpha^{k-1} + \mathcal{G}(a_0, \cdots, a_{k-1})) + 1, \qquad (7)$$

where the word-level specification polynomial $\mathcal{F}(A)$ gets reduced to a polynomial expression $\mathcal{G}(a_0, \dots, a_{k-1})$ in primary input bits. Due to RTTO >, subsequent divisions of the above remainder in Eqn. (7) by $\{f_1, \dots, f_s\}$ will successively cancel the terms in variables $z_i, i = 0, \dots, k-1$, and express them in terms of the primary input bits. Since primary input bits are last in RTTO >, they never appear as leading terms in any of the polynomials in $J_L$; so the terms in primary input bits cannot be canceled. As a result, after complete reduction of $Spoly(f_m, f_o)$ by $J_L + J_0$, the remainder will be a polynomial expression of the form $Spoly(f_m, f_o)$ $\xrightarrow{J_L+J_0}+_+$ $h = t \cdot r + 1$, where $r$ is a polynomial only in bit-level primary input variables. $\square$

Coming back to the computation $GB(J_L + J_0)$, the polynomial $h$ is now added to the current basis, i.e. $G = \{J_L + J_0\} \cup \{h\}$ in Buchberger's algorithm (Line 7 in Alg. 1). This polynomial $h$ now needs to be paired with other polynomials in the basis. There are only two sets of possibilities for subsequent critical pairings: i) the pair $Spoly(f_m, h)$; and ii) to pair $h$ with corresponding vanishing polynomials from the ideal $J_0$. For all other polynomials $f_i \in \{f_1, \dots, f_s\}$, $lm(h)$ and $lm(f_i)$ have relatively prime leading terms, so $Spoly(h, f_i)_{i=1,\dots,s} \xrightarrow{J_L+J_0}+_0$ 0; so the pairs $(h, f_i)$ need not be considered in $GB(J_L + J_0)$.
We now show that $Spoly(f_m, h) \xrightarrow{G=\{J_L+J_0\}\cup\{h\}}_+ 0$, so the pair $(f_m, h)$ also need not be considered.

From Lemma 7.2 and its proof, we have that $h = t \cdot r + 1$ and $Z + Z_S \xrightarrow{G=\{J_L+J_0\}}_+ r$, with $r$ composed of primary input bits. Let $r = e + r'$, where $e = lt(r)$ is the leading term and $r' = r - e$ is tail($r$), both expressed in primary input bits. With this notation, $h = te + tr' + 1$ and $lt(h) = te$. The LCM $L$ of leading monomials of $f_m$ and $h$ is $L = LCM(lm(f_m), lm(h)) = LCM(tZ, te) = tZe$. Consider the computation $Spoly(f_m, h)$:

$$ 
\begin{aligned}
Spoly(f_m, h) &= \frac{L}{lt(f_m)} \cdot f_m - \frac{L}{lt(h)} \cdot h \\
&= ef_m + Zh = e(tZ + tZ_S + 1) + Z(te + tr' + 1) \\
&= tr'Z + teZ_S + Z + e
\end{aligned}
\qquad (8) $$

Next consider the reduction of $Spoly(f_m, h)$ by $\{J_L + J_0\} \cup \{h\}$, where $h$ itself is used in the division. The reduction $Spoly(f_m, h) \xrightarrow{h} _+$ is computed as,

$$ 
\begin{aligned}
tr'Z + teZ_S + Z + e &\xrightarrow{h} _+ tr'Z + (tr' + 1)Z_S + Z + e \\
&= tr'(Z + Z_S) + Z + Z_S + e \\
&= (tr' + 1)(Z + Z_S) + e
\end{aligned}
\qquad (9) $$

Reducing the intermediate remainder of Eqn. (9) by the polynomials in $J_L + J_0$ results in $(tr' + 1)(r) + e$. This reduction process is similar to the one in the proof of Lemma 7.2. Now consider the polynomial $(tr' + 1)(r) + e$

$$ 
\begin{aligned}
(tr' + 1)(r) + e &= (tr' + 1)(e + r') + e \\
&= ter' + tr'^2 + e + r' + e \\
&= ter' + tr'^2 + r'
\end{aligned}
\qquad (10) $$

The polynomial in Eqn. (10) can be further reduced by $h$ which results in 0 implying that $Spoly(f_m, h) \xrightarrow{\{J_L+J_0\}\cup\{h\}}_+ 0$.

$$ 
\begin{aligned}
ter' + tr'^2 + r' &\xrightarrow{h} _+ (tr' + 1)r' + tr'^2 + r' \\
&= tr'^2 + r' + tr'^2 + r' = 0
\end{aligned}
$$

In summary, we have shown that to compute $E_L$ as $GB(J_L + J_0) \cap \mathbb{F}_{2^k}[X_{PI}]$, we only need to compute $Spoly(f_m, f_o) \xrightarrow{J_L+J_0} _+ h$, and pair $h$ with polynomials of $J_0$, as all other $Spoly(h, f_i)$ reduce to 0. This gives us the following procedure to compute the Gröbner basis of $E_L$ (respectively $E_H$):

1. Compute $Spoly(f_o, f_m) \xrightarrow{J_L+J_0} _+ h$, where $(f_m, f_o)$ is the only pair of polynomials in $J_L + J_0$ that do not have relatively prime leading monomials.

2. Use Buchberger's algorithm to compute GB of the set of vanishing polynomials and $h$, i.e. compute $G = GB(J_0 = \{x_i^2 - x_i : x_i \in X_{PI}\}, h)$.

3. From $G$, collect the polynomials not containing $t$; i.e $E_L = G \cap \mathbb{F}_{2^k}[X_{PI}]$. These polynomials generate the ideal $E_L$.
The same technique is also used to compute $E_H$ by replacing $J_L$ with $J_H$ in the above procedure. In our approach, we use the above procedures to compute $E_L, E_H$ for Thm. 5.1 and then compute $U(X_{PI})$ from $E_L$ using Alg. 2.

## 8 Experimental Results

We have performed rectification experiments on finite field arithmetic circuits that are used in cryptography, where the implementation is different from the specification due to exactly one gate. This is to ensure that single-fix rectification is feasible for such bugs, so that a rectification function can be computed. We have implemented the procedures described in the previous sections — i.e. the concepts of Thm. 5.1, Section 7 and Alg. 2 — using the SINGULAR symbolic algebra computation system [ver. 4-1-0][41]. Given a *Spec*, a buggy *Impl* circuit *C*, and the set *X* of rectification targets, our approach checks for each net $x_i \in X$ if single-fix rectification is feasible, and if so, computes a rectification function $x_i = U(X_{PI})$. The experiments were conducted on a desktop computer with a 3.5GHz Intel Core™ i7-4770K Quad-core CPU, 16 GB RAM, running 64-bit Linux OS.

Experiments are performed with three different types of finite field circuit benchmarks. Two of these are the Mastrovito and the Montgomery multiplier circuit architectures used for modular multiplication. Mastrovito multipliers compute $Z = A \times B$ (mod $P(x)$) where $P(x)$ is a given primitive polynomial for the datapath size $k$. Montgomery multipliers are instead preferred for exponentiation operations (often required in cryptosystems). The last set of benchmarks are circuits implementing point addition over elliptic curves used for encryption, decryption and authentication in elliptic curve cryptography (ECC).

<table><caption>Table 1: Mastrovito multiplier rectification against Montgomery multiplier specification. Time in seconds; Time-out = 5400s; k: Operand width</caption><thead><tr><th rowspan="2">k</th><th colspan="2"># of Gates</th><th rowspan="2">SAT</th><th rowspan="2">Thm. 5.1</th><th rowspan="2">Alg. 2</th><th rowspan="2">Mem</th></tr><tr><th>Mas</th><th>Mont</th></tr></thead><tbody><tr><td>4</td><td>48</td><td>96</td><td>0.09</td><td>0.03</td><td>0.001</td><td>8.16 MB</td></tr><tr><td>8</td><td>292</td><td>319</td><td>158.34</td><td>0.41</td><td>0.006</td><td>20.36 MB</td></tr><tr><td>9</td><td>237</td><td>396</td><td>4,507</td><td>0.47</td><td>0.001</td><td>18.95 MB</td></tr><tr><td>10</td><td>285</td><td>480</td><td>TO</td><td>0.84</td><td>0.001</td><td>28.2 MB</td></tr><tr><td>16</td><td>1,836</td><td>1,152</td><td>TO</td><td>73.63</td><td>0.024</td><td>0.32 GB</td></tr><tr><td>32</td><td>5,482</td><td>4,352</td><td>TO</td><td>3621</td><td>0.043</td><td>2.4 GB</td></tr></tbody></table>

First we present the results for the case where the reference *Spec* is given as a Montgomery multiplier, and the buggy implementation is given as a Mastrovito multiplier, which is to be rectified. Thm. 5.1, along with efficient GB-computation of the ideals $E_L, E_H$, is applied at a net $x_i \in X$, such that the circuit is rectifiable at $x_i$. Table 1 compares the execution time for the SAT-based approach of [16] against ours (Thm. 5.1) for checking whether a buggy Mastrovito multiplier can be rectified at a certain location in the circuit against a Montgomery multiplier specification. The SAT procedure is implemented using the *abc* tool [42]. We execute the command *inter* on the ON set and
OFF set as described in [16]. The SAT-based procedure is unable to perform the necessary unsatisfiability check for circuits beyond 9-bit operand word-lengths, whereas our approach easily scales to 32-bit circuits. Using our approach, the polynomial $U(X_{PI})$ needed for rectification is computed from $E_L$ and the time is reported in Table 1 in the Alg. 2 column. The last column in the table shows the memory usage of our approach.

We also perform the rectification when the *Spec* is given as a polynomial expression instead of a circuit. Table 2 shows the results for checking whether the incorrect Mastrovito implementation can be single-fix rectified against the word-level specification polynomial $f_{spec} : Z_S + A \cdot B$.

<table><caption>Table 2: Mastrovito multiplier rectification against polynomial specification $Z_S = AB$. Time in seconds; Time-out = 5400s; k: Operand width</caption><thead><tr><th>k</th><th># of Gates</th><th>Thm. 5.1</th><th>Alg. 2</th><th>Mem</th></tr></thead><tbody><tr><td>4</td><td>48</td><td>0.01</td><td>0.001</td><td>7.24 MB</td></tr><tr><td>8</td><td>292</td><td>0.08</td><td>0.006</td><td>14.95 MB</td></tr><tr><td>16</td><td>1,836</td><td>4.83</td><td>0.038</td><td>0.2 GB</td></tr><tr><td>32</td><td>5,482</td><td>100.52</td><td>0.015</td><td>1.42 GB</td></tr><tr><td>64</td><td>21,813</td><td>4,989</td><td>0.117</td><td>12.25 GB</td></tr></tbody></table>

Point addition is an important operation required for the task of encryption, decryption and authentication in ECC. Modern approaches represent the points in projective coordinate systems, e.g., the López-Dahab (LD) projective coordinate [43], due to which the operations can be implemented as polynomials in the field.

<table><caption>Table 3: Point Addition circuit rectification against polynomial specification $D = B^2$. (C + aZ_1^2)$. Time in seconds; Time-out = 5400s; k: Operand width</caption><thead><tr><th>k</th><th># of Gates</th><th>Thm. 5.1</th><th>Alg. 2</th><th>Mem</th></tr></thead><tbody><tr><td>8</td><td>243</td><td>0.05</td><td>0.022</td><td>9.73 MB</td></tr><tr><td>16</td><td>1,277</td><td>3.48</td><td>0.019</td><td>88.78 MB</td></tr><tr><td>32</td><td>3,918</td><td>86.75</td><td>0.028</td><td>0.47 GB</td></tr><tr><td>64</td><td>1,5305</td><td>4,923</td><td>0.053</td><td>7.13 GB</td></tr></tbody></table>

**Example 8.1.** Consider point addition in López-Dahab (LD) projective coordinate. Given an elliptic curve: $Y^2 + XYZ = X^3Z + aX^2Z^2 + bZ^4$ over $\mathbb{F}_{2^k}$, where X, Y, Z are k-bit vectors that are elements in $\mathbb{F}_{2^k}$ and similarly, a, b are constants from the field. We represent point addition over the elliptic curve as $(X_3, Y_3, Z_3) = (X_1, Y_1, Z_1) + (X_2, Y_2, 1)$. Then $X_3, Y_3, Z_3$ can be computed as follows:

$$A = Y_2 \cdot Z_1^2 + Y_1$$

$$C = Z_1 \cdot B$$

$$Z_3 = C^2$$

$$X_3 = A^2 + D + E$$

$$G = X_3 + Y_2 \cdot Z_3$$

$$B = X_2 \cdot Z_1 + X_1$$

$$D = B^2 \cdot (C + aZ_1^2)$$

$$E = A \cdot C$$

$$F = X_3 + X_2 \cdot Z_3$$

$$Y_3 = E \cdot F + Z_3 \cdot G$$
Each of the polynomials in the above design are implemented as (gate-level) logic
blocks and are interconnected to obtain final outputs X₃, Y₃ and Z₃. Table 3 shows the
results for the block that computes $D = B^2 \cdot (C + aZ_1^2)$. Our approach can rectify up to
64-bit circuits.

*Limitations of our approach:* We also performed experiments where we apply Thm. 5.1 at a gate output which *cannot* rectify the circuit. We used the Montgomery multiplier as the specification and a Mastrovito multiplier as the implementation. For 4- and 8-bit word-lengths, the execution time of our approach was comparable to that of the SAT-based approach, and was ~ 0.1 seconds. For the 16-bit multipliers, the SAT-based approach completed in 0.11 seconds. On the other hand, application of Thm. 5.1 resulted in a memory explosion and consumed ~ 30 GB of memory within 5-6 minutes. This is due to the fact that when $1 \notin E_L + E_H$, then $GB(E_L + E_H)$ is not equal to $\{1\}$ and the Gröbner basis algorithm produces a very large output. To improve our approach we are working on term ordering heuristics so that our approach can perform efficiently in both cases. We also wish to employ other data-structures better suited to circuits, as SINGULAR's data structure is not very memory efficient. SINGULAR also has an upper limit on the number of variables (32,768) that can be accommodated in the system, limiting application to larger circuits.

9 Conclusion

This paper considers single-fix rectification of arithmetic circuits. The approach is ap-
plied after formal verification detects the presence of a bug in the design. We assume
that post-verification debugging has been performed a set (X) of nets is provided as
rectification targets. The paper presents necessary and sufficient conditions that ascer-
tains whether a buggy circuit can be single-fix rectified at a net xᵢ ∈ X. When single-fix
rectification is feasible, we compute a rectification polynomial function xᵢ = U(XPI),
which can be synthesized into a circuit. For this purpose, the paper introduces the no-
tion of Craig interpolants in algebraic geometry in finite fields, proves their existence,
and gives an effective procedure for their computation. Furthermore, we show how the
rectification polynomial can be computed from algebraic interpolants. Experiments are
performed over various finite field arithmetic circuits that show the efficiency of our ap-
proach as against SAT-based approaches. Limitations of our approach are also analyzed.
We are currently investigating the extension of our approach to multi-fix rectification.

References

1. D. Ritirc, A. Biere, and M. Kauers, “Column-Wise Verification of Multipliers Using Computer Algebra,” in *Formal Methods in Computer-Aided Design (FMCAD)*, 2017, pp. 23–30.

2. M. Ciesielski, C. Yu, W. Brown, D. Liu, and A. Rossi, “Verification of Gate-level Arithmetic Circuits by Function Extraction,” in *52nd ACM/EDAC/IEEE Design Automation Conference (DAC)*, 2015, pp. 1–6.

3. A. Sayed-Ahmed, D. Große, U. Kühne, M. Soeken, and R. Drechsler, “Formal Verification of Integer Multipliers by Combining Gröbner Basis with Logic Reduction,” in *Design, Automation Test in Europe Conference Exhibition (DATE)*, 2016, pp. 1048–1053.
4. O. Wienand, M. Wedler, D. Stoffel, W. Kunz, and G. Gruel, "An Algebraic Approach to Prov-
ing Data Correctness in Arithmetic Datapaths," in *Computer Aided Verification Conference*,
2008, pp. 473–486.

5. N. Shekhar, P. Kalla, and F. Enescu, "Equivalence Verification of Polynomial Datapaths using Ideal Membership Testing," *IEEE Transactions on CAD*, vol. 26, no. 7, pp. 1320–1330, July 2007.

6. N. Tew, P. Kalla, N. Shekhar, and S. Gopalakrishnan, "Verification of Arithmetic Datapaths using Polynomial Function Models and Congruence Solving," in *Proc. Intl. Conf. on Computer-Aided Design (ICCAD)*, 2008, pp. 122–128.

7. J. Lv, P. Kalla, and F. Enescu, "Efficient Gröbner Basis Reductions for Formal Verification of Galois Field Arithmetic Circuits," in *IEEE Trans. on CAD*, vol. 32, no. 9, 2013, pp. 1409–1420.

8. T. Pruss, P. Kalla, and F. Enescu, "Efficient Symbolic Computation for Word-Level Abstraction from Combinational Circuits for Verification over Finite Fields," *IEEE Trans. on CAD*, vol. 35, no. 7, pp. 1206–1218, July 2016.

9. A. Lvov, L. Lastras-Montano, B. Trager, V. Paruthi, R. Shadowen, and A. El-Zein, "Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry," *Formal Methods in System Design*, vol. 45, no. 2, pp. 189–212, Oct 2014.

10. X. Sun, P. Kalla, T. Pruss, and F. Enescu, "Formal verification of sequential galois field arithmetic circuits using algebraic geometry," in *Proc. Design, Automation and Test in Europe*, 2015.

11. D. Cox, J. Little, and D. O'Shea, *Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra*. Springer, 2007.

12. W. W. Adams and P. Loustaunau, *An Introduction to Gröbner Bases*. American Mathematical Society, 1994.

13. J. C. Madre, O. Coudert, and J. P. Billon, "Automating the Diagnosis and the Rectification of Design Errors with PRIAM," in *Proc. ICCAD*, 1989, pp. 30–33.

14. C. C. Lin, K. C. Chen, S. C. Chang, and M. Marek-Sadowska, "Logic Synthesis for Engineering Change," in *Proc. Design Automation Conf. (DAC)*, 1995, pp. 647–652.

15. C. Scholl and B. Becker, "Checking Equivalence for Partial Implementations," in *Design Automation Conference (DAC)*, 2001.

16. K. F. Tang, C. A. Wu, P. K. Huang, and C. Y. Huang, "Interpolation-Based Incremental ECO Synthesis for Multi-Error Logic Rectification," in *Proc. Design Automation Conf. (DAC)*, 2011, pp. 146–151.

17. W. Craig, "Linear reasoning: A new form of the Herbrand-Gentzen theorem," *Journal of Symbolic Logic*, vol. 22, no. 3, pp. 250–268, 1957.

18. H. T. Liaw, J. H. Tsaih, and C. S. Lin, "Efficient Automatic Diagnosis of Digital Circuits," in *Proc. ICCAD*, 1990, pp. 464–467.

19. K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, and B. Becker, "Equivalence Checking of Partial Designs Using Dependency Quantified Boolean Formulae," in *IEEE International Conference on Computer Design (ICCD)*, 2013.

20. S. Jo, T. Matsumoto, and M. Fujita, "SAT-Based Automatic Rectification and Debugging of Combinational Circuits with LUT Insertions," in *IEEE 21st Asian Test Symposium*, 2012.

21. M. Fujita and A. Mishchenko, "Logic Synthesis and Verification on Fixed Topology," in *22nd International Conference on Very Large Scale Integration (VLSI-SoC)*, 2014.

22. M. Fujita, "Toward Unification of Synthesis and Verification in Topologically Constrained Logic Design," *Proceedings of the IEEE*, 2015.

23. B. H. Wu, C. J. Yang, C. Y. Huang, and J. H. R. Jiang, "A Robust Functional ECO Engine by SAT Proof Minimization and Interpolation Techniques," in *Intl. Conf. on Comp. Aided Des.*, 2010, pp. 729–734.
24. A. C. Ling, S. D. Brown, S. Safarpour, and J. Zhu, "Toward Automated ECOs in FPGAs," *IEEE Trans. CAD*, vol. 30, no. 1, pp. 18-30, 2011.

25. A. Q. Dao, N.-Z. Lee, L.-C. Chen, M. P.-H. Lin, J.-H. R. Jiang, A. Mishchenko, and R. Brayton, "Efficient Computation of ECO Patch Functions," in *55th Design Automation Conference (DAC)*, Jun 2018, pp. 51:1-51:6.

26. U. Gupta, I. Ilioaea, R. V., S. A., P. Kalla, and F. Enescu, "On the Rectifiability of Arithmetic Circuits using Craig Interpolants in Finite Fields," in *Intl. Conf. on Very Large Scale Integration (VLSI-SoC)*, 2018, pp. 49-54.

27. S. Ghandali, C. Yu, D. Liu, W. Brown, and M. Ciesielski, "Logic Debugging of Arithmetic Circuits," in *IEEE Computer Society Annual Symposium on VLSI*, 2015.

28. F. Farahmandi and P. Mishra, "Automated Debugging of Arithmetic Circuits Using Incremental Gröbner Basis Reduction," in *IEEE International Conference on Computer Design (ICCD)*, 2017.

29. ——, "Automated Test Generation for Debugging Arithmetic Circuits," in *Des. Auto. Test in Eur. Conf. (DATE)*, 2016.

30. K. L. McMillan, "Interpolation and SAT-Based Model Checking," in *Computer Aided Verification*, July 2003, pp. 1-13.

31. R.-R. Lee, J.-H. R. Jiang, and W.-L. Hung, "Bi-Decomposing Large Boolean Functions via Interpolation and Satisfiability Solving," in *Proc. Design Automation Conference (DAC)*, 2008, pp. 636-641.

32. K. McMillan, "An Interpolating Theorem Prover," *Theoretical Computer Science*, vol. 345, no. 1, pp. 101-121, 2005, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004).

33. D. Kapur, R. Majumdar, and G. Zarba, "Interpolation for Data-structures," in *Proc. ACM SIGSOFT Intl. Symp. on Found. of Soft. Eng.*, 2006, pp. 105-116.

34. A. Cimatti, A. Griggio, and R. Sebastiani, "Efficient Interpolant Generation in Satisfiability Modulo Theories," in *Tools and Algorithms for the Construction and Analysis of Systems (TACAS)*, 2008, pp. 397-412.

35. A. Griggio, "Effective Word-level Interpolation for Software Verification," in *Formal Methods in Computer-Aided Design (FMCAD)*, 2011, pp. 28-36.

36. S. Gao, A. Platzer, and E. Clarke, "Quantifier Elimination over Finite Fields with Gröbner Bases," in *Algebraic Informatics: 4th International Conference, CAI*, 2011, pp. 140-157.

37. S. Gao, "Counting Zeros over Finite Fields with Gröbner Bases," Master's thesis, Carnegie Mellon University, 2009.

38. J. Lv, "Scalable Formal Verification of Finite Field Arithmetic Circuits using Computer Algebra Techniques," Ph.D. dissertation, Univ. of Utah, Aug. 2012.

39. B. Buchberger, "Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal," Ph.D. dissertation, University of Innsbruck, 1965.

40. ——, "A criterion for detecting unnecessary reductions in the construction of a groebner bases," in *EUROSAM*, 1979.

41. W. Decker, G.-M. Greuel, G. Pfister, and H. Schönemann, "SINGULAR 4-1-0 — A computer algebra system for polynomial computations," http://www.singular.uni-kl.de, 2016.

42. R. Brayton and A. Mishchenko, "ABC: An Academic Industrial-Strength Verification Tool," in *Comp. Aid. Verif.*, vol. 6174, 2010, pp. 24-40.

43. J. López and R. Dahab, "Improved Algorithms for Elliptic Curve Arithmetic in GF(2"), in *Proceedings of the Selected Areas in Cryptography*. London, UK, UK: Springer-Verlag, 1999, pp. 201-212.