We present an approach to partial logic synthesis of arithmetic circuits. Its targeted applications are rectification of buggy circuits, and computing care and don't care sets at internal nets of the circuit. The approach models the circuit by way of polynomial ideals in rings with coefficients in the field of rationals (ℚ). Techniques from commutative algebra are applied to compute internal patch functions as polynomials over ℚ. We describe how the care set and the don't care conditions manifest in the algebraic setting, and show how to generate corresponding Boolean functions from polynomials over ℚ. Experiments are conducted over various integer multiplier architectures which demonstrate the efficacy of our approach, where SAT/interpolation based techniques are infeasible.

This paper proposes a symbolic algebra approach for multi-target rectification of integer arithmetic circuits. The circuit is represented as a system of polynomials and rectified against a polynomial specification with computations modeled over the field of rationals. Given a set of nets as potential rectification targets, we formulate a check to ascertain the existence of rectification functions at these targets. Upon confirmation, we compute the patch functions collectively for the targets. In this regard, we show how to synthesize a logic sub-circuit from polynomial artifacts generated over the field of rationals. We present new mathematical contributions and results to substantiate this synthesis process. We present two approaches for patch function computation: a greedy approach that resolves the rectification functions for the targets and an approach that explores a subset of don’t care conditions for the targets. Our approach is implemented as custom software and utilizes the existing open-source symbolic algebra libraries for computations. We present experimental results of our approach on several integer multipliers benchmark and discuss the quality of the patch sub-circuits generated.

This paper addresses the rectification of faulty finite field arithmetic circuits by computing patch functions at internal nets using techniques from polynomial algebra. Contemporary approaches that utilize SAT solving and Craig interpolation are infeasible in rectifying arithmetic circuits. Given candidate nets, prior algebra-based techniques can ascertain whether the circuit admits multi-fix rectification at these nets but cannot compute patch functions. We show how the algebraic computing model facilitates the exploration of admissible rectification functions, collectively, for the nets. This model also enables the exploitation of don’t care conditions for the synthesis and realization of the patches. Experimental results on large operand width finite field benchmarks, as used in cryptography, substantiate our approach.

When formal verification identifies the presence of a bug in a design, it is required to rectify the circuit at some net(s). Modern approaches formulate the rectification test as an unsatisfiability proof, and then use Craig interpolants (CI) in propositional logic to compute the corresponding rectification functions. Boolean SAT and CI engines are infeasible in rectification of finite field arithmetic circuits, where polynomial algebra is more suitable. Recently, it was shown that CI exist in polynomial algebra in finite fields. This paper presents a detailed theory and algorithms for CI in finite fields, and characterizes the lattice of all algebraic interpolants. Using the Gröbner basis algorithm, we present techniques to traverse the interpolant lattice. This allows to explore various interpolants for efficient synthesis of rectification functions for finite field arithmetic circuits. Experimental results are presented that demonstrate the efficacy of our approach.

Formal verification of arithmetic circuits checks whether or not a gate-level circuit correctly implements a given specification model. In cases where this equivalence check fails - the presence of a bug is detected - it is required to: i) debug the circuit, ii) identify a set of nets (signals) where the circuit might be rectified, and iii) compute the corresponding rectification functions at those locations. This paper addresses the problem of post-verification debugging and correction (rectification) of finite field arithmetic circuits. The specification model and the circuit implementation may differ at any number of inputs. We present techniques that determine whether the circuit can be rectified at one particular net (gate output) - i.e. we address single-fix rectification.Starting from an equivalence checking setup modeled as a polynomial ideal membership test, we analyze the ideal membership residue to identify potential single-fix rectification locations. Subsequently, we use Nullstellensatz principles to ascertain if indeed a single-fix rectification can be applied at any of these locations. If a single-fix rectification exists, we derive a rectification function by modeling it as the synthesis of an unknown component problem. Our approach is based upon the Gröbner basis algorithm, which we use both as a decision procedure (for rectification test) as well as a quantification procedure (for computing a rectification function). Experiments are performed over various finite field arithmetic circuits that demonstrate the efficacy of our approach, whereas SAT-based approaches are infeasible.

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. This paper addresses 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 location, formulated as the Weak Nullstellensatz test. 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. Experimental results demonstrate the superiority of our approach against SAT-based approaches.

This paper introduces a technique to derive a word-level abstraction of the function implemented by a combinational logic circuit. The abstraction provides a canonical representation of the function as a polynomial${Z} {= {\mathcal {F}}(A)}$over the finite field$ {{\mathbb {F}}_{2^{k}}}$, where${Z}$and$ {A}$represent the${k}$-bit output and input bit-vectors (words) of the circuit, respectively. This canonical abstraction can be utilized for formal verification and equivalence checking of combinational circuits. Our approach to abstraction is based upon concepts from computational commutative algebra and algebraic geometry. We show that the abstraction${Z} {= {\mathcal {F}}(A)}$can be derived by computing a Gröbner basis of the polynomials corresponding to the circuit, using a specific elimination term order derived from the circuit’s topology. Computing Gröbner bases using elimination term orders is infeasible for large circuits. To overcome this limitation, we describe an efficient symbolic computation to derive the word-level polynomial. Our algorithms exploit: 1) the structure of the circuit; 2) the properties of Gröbner bases; 3) characteristics of finite fields$ {{\mathbb {F}}_{2^{k}}}$; and 4) modern algorithms from symbolic algebra, to derive the canonical polynomial representation. This approach is employed to verify (and detect bugs in) large combinational finite field arithmetic circuits, where contemporary verification techniques are known to be infeasible.

Custom arithmetic circuits designed over Galois fields F2k are prevalent in cryptography, where the field size k is very large (e.g. k = 571-bits). Equivalence checking of such large custom arithmetic circuits against baseline golden models is beyond the capabilities of contemporary techniques. This paper addresses the problem by deriving word-level canonical polynomial representations from gate-level circuits as Z = F (A) over F2k, where Z and A represent the output and input bit-vectors of the circuit, respectively. Using algebraic geometry, we show that the canonical polynomial abstraction can be derived by computing a Gröbner basis of a set of polynomials extracted from the circuit, using a specific elimination (abstraction) term order. By efficiently applying these concepts, we can derive the canonical abstraction in hierarchically designed, custom arithmetic circuits with up to 571-bit datapath, whereas contemporary techniques can verify only up to 163-bit circuits.

Galois field arithmetic is a critical component in communication and security-related hardware, requiring dedicated arithmetic architectures for better performance. In many Galois field applications, such as cryptography, the data-path size in the circuits can be very large. Formal verification of such circuits is beyond the capabilities of contemporary verification techniques. This paper addresses formal verification of combinational arithmetic circuits over Galois fields of the type${\BBF}_{2^{k}}$using a computer-algebra/algebraic-geometry-based approach. The verification problem is formulated as membership testing of a given specification polynomial in a corresponding ideal generated by the circuit constraints. Ideal membership testing requires the computation of a Gröbner basis, which is computationally very expensive. To overcome this limitation, we analyze the circuit topology and derive a term order to represent the polynomials. Subsequently, using the theory of Gröbner bases over${\BBF}_{2^{k}}$, we show that this term order renders the set of polynomials itself a minimal Gröbner basis of this ideal. Consequently, the verification test reduces to a much simpler case of Gröbner basis reduction via polynomial division, significantly enhancing verification efficiency. To further improve our approach, we exploit the concepts presented in the$F4$algorithm for Gröbner basis, and show that the verification test can be formulated as Gaussian elimination on a matrix representation of the problem. Finally, we demonstrate the ability of our approach to verify the correctness of, and detect bugs in, up to 163-bit circuits in${\BBF}_{2^{163}}$—whereas verification utilizing contemporary techniques proves infeasible.

Galois field arithmetic finds application in many areas, such as cryptography, error correction codes, signal processing, etc. Multiplication lies at the core of most Galois field computations. This paper addresses the problem of formal verification of hardware implementations of (modulo) multipliers over Galois fields of the type F(2k), using a computer-algebra/algebraic-geometry based approach. The multiplier circuit is modeled as a polynomial system in F(2k)[x1, x2, ... , xd] and the verification problem is formulated as a membership test in a corresponding (radical) ideal. This requires the computation of a Gröbner basis, which can be computationally intensive. To overcome this limitation, we analyze the circuit topology and derive a term order to represent the polynomials. Subsequently, using the theory of Gröbner bases over Galois fields, we prove that this term order renders the set of polynomials itself a Gröbner basis of this ideal - thus significantly improving verification. Using our approach, we can verify the correctness of, and detect bugs in, upto 163-bit circuits in F(2163); whereas contemporary approaches are infeasible.

This paper addresses simulation-based verification of high-level [algorithmic, behavioral, or register-transfer level (RTL)] descriptions of arithmetic datapaths that perform polynomial computations over finite word-length operands. Such designs are typically found in digital signal processing (DSP) for audio/video and multimedia applications; where the word-lengths of input and output signals (bit-vectors) are predetermined and fixed according to the desired precision. Initial descriptions of such systems are usually specified as Matlab/C code. These are then automatically translated into behavioral/RTL descriptions for subsequent hardware synthesis. In order to verify that the initial Matlab/C model is bit-true equivalent to the translated RTL, how many simulation vectors need to be applied? This paper derives some important results that show that exhaustive simulation is not necessary to prove/disprove their equivalence. To derive these results, we model the datapath computations as polynomial functions over finite integer rings of the form , where corresponds to the bit-vector word-length. Subsequently, by exploring some number theoretic and algebraic properties of these rings, we derive an upper bound on the number of simulation vectors required to prove equivalence or to identify bugs. Moreover, these vectors cannot be arbitrarily generated. We identify exactly those vectors that need to be simulated. Experiments are performed within practical computer-aided design (CAD) settings to demonstrate the validity and applicability of these results.

This paper presents an approach to area optimization of arithmetic datapaths that perform polynomial computations over bit-vectors with finite widths. Examples of such designs abound in DSP for audio, video and multimedia computations where the input and output bit-vector sizes are dictated by the desired precision. A bit-vector of size m represents integer values reduced modulo 2m(%2m). Therefore, finite word-length bit-vector arithmetic can be modeled as algebra over finite integer rings, where the bit-vector size dictates the ring cardinality. This paper demonstrates how the number-theoretic properties of finite integer rings can be exploited for optimization of bit-vector arithmetic. Along with an analytical model to estimate the implementation cost at RTL, two algorithms are presented to optimize bit-vector arithmetic. Experimental results, conducted within practical CAD settings, demonstrate significant area savings due to our approach.

Polynomial computations over fixed-size bitvectors are found in many practical datapath designs. For efficient RTL synthesis, it is important to identify good decompositions of the polynomial into smaller/simpler units. Symbolic computer algebra algorithms and tools have been used for this purpose. However, fixed-size (m) bit-vector arithmetic is polynomial algebra over the finite integer ring Z2m, which is a non-unique factorization domain (non-UFD). While non-UFDs provide an extra freedom to search for decompositions, they complicate polynomial manipulation as traditional division-based algorithms are inapplicable. This paper presents new mathematical concepts for polynomial decomposition over Z2m, for RTL synthesis over fixedsize m-bit vectors. Given a polynomial, we identify a specific set of linear expressions and compute the Gröbner bases of their ideal (over non-UFD Z2m) using syzygies. This basis serves as good building-blocks for the given computation. A decomposition is identified by subsequent Gröbner basis reduction. Experimental results demonstrate significant area savings due to our approach, as compared against contemporary datapath synthesis techniques.

This paper addresses the equivalence verification problem of register-transfer level (RTL) descriptions that implement arithmetic computations (such as add, mult) over bit vectors with finite widths. A bit vector of size represents integer values from 0 to 2m-1, implying that the corresponding integer values are reduced modulo 2m(%2m). This suggests that bit-vector arithmetic can be efficiently modeled as algebra over finite integer rings, where the bit-vector size (m) dictates the cardinality of the ring (Z2m). This paper models the arithmetic datapath verification problem as the equivalence testing of polynomial functions from Z2n1timesZ2n2times...timesZ2ndrarrZ2m. We formulate the equivalence problem into that of proving whether f-gequiv0%2m. Fundamental concepts and results from ldquonumber,rdquo ldquoring,rdquo and ldquoideal theoryrdquo are subsequently employed to develop systematic complete algorithmic procedures to solve the problem. We demonstrate the application of the proposed theoretical concepts to high-level (behavioral/RTL) verification of bit-vector arithmetic within practical computer-aided design settings. Using our approach, we verify a set of arithmetic datapaths at RTL, where contemporary verification approaches prove to be infeasible.

This paper addresses the problem of equivalence verification of RTL descriptions that implement arithmetic computations (add, mult, shift) over bit-vectors that have differing bit-widths. Such designs are found in many DSP applications where the widths of input and output bit-vectors are dictated by the desired precision. A bit-vector of size n can represent integer values from 0 to 2n- 1; i.e. integers reduced modulo 2n. Therefore, to verify bit-vector arithmetic over multiple word-length operands, we model the RTL datapath as a polynomial function from Z2n1times Z2n2times ... Z2ndto Z2m. Subsequently, RTL equivalence f equiv g is solved by proving whether (f - g) equiv 0 over such mappings. Exploiting concepts from number theory and commutative algebra, a systematic, complete algorithmic procedure is derived for this purpose. Experimentally, we demonstrate how this approach can be applied within a practical CAD setting. Using our approach, we verify a set of arithmetic datapaths at RTL where contemporary approaches prove to be in feasible

This paper addresses simulation-based verification of high-level descriptions of arithmetic datapaths. Instances of such designs are commonly found in DSP for audio, video and multimedia applications, where the word-lengths of input/output bit-vectors are fixed according to the desired precision. Initial descriptions of such systems are usually specified as Matlab/C code. These are then automatically translated into behavioural/RTL descriptions (HDL) for subsequent hardware synthesis. In order to verify that the initial Matlab/C model is bit-true equivalent to the translated RTL, how many simulation vectors need to be applied? This paper explores results from number theory and commutative algebra to show that exhaustive simulation is not necessary for testing their equivalence. In particular, we derive an upper bound on the number of simulation vectors required to prove equivalence or identify bugs. These vectors cannot be arbitrarily generated; we determine exactly those vectors that need to be simulated. Extensive experiments are performed within practical CAD settings to demonstrate the validity and applicability of these results

This paper addresses the problem of equivalence verification of RTL descriptions. The focus is on datapath-oriented designs that implement polynomial computations over fixed-size bit-vectors. When the size (m) of the entire datapath is kept constant, fixed-size bit-vector arithmetic manifests itself as polynomial algebra over finite integer rings of residue classes Z/sub 2//sup m/. The verification problem then reduces to that of checking equivalence of multi-variate polynomials over Z/sub 2//sup m/. This paper exploits the concepts of polynomial reducibility over Z/sub 2//sup m/ and derives an algorithmic procedure to transform a given polynomial into a unique canonical form modulo 2/sup m/. Equivalence testing is then carried out by coefficient matching. Experiments demonstrate the effectiveness of our approach over contemporary techniques.

This paper addresses the problem of equivalence verification of high-level/RTL descriptions. The focus is on datapath-oriented designs that implement univariate polynomial computations over fixed-size bit-vectors. When the size (m) of the entire datapath is kept constant, fixed-size bit-vector arithmetic manifests itself as polynomial algebra over finite integer rings of residue classes Z/sub 2//sup m/. The verification problem then reduces to that of checking equivalence of over Z/sub 2//sup m/ in other words, to prove f(x)%2/sup m/ /spl equiv/ g(x)%2/sup m/. This paper transforms the equivalence verification problem into proving (f(x) - g(x))%2/sup m/ /spl equiv/ 0. Exploiting the theory of vanishing polynomials over finite integer rings, a systematic algorithmic procedure is derived to establish whether or not a given polynomial vanishes (always evaluates to 0) over Z/sub 2//sup m/. Experiments demonstrate the effectiveness of our approach over contemporary techniques.