The paper addresses the formal verification of gate-level square-root circuits. Division and square root functions are some of the most complex arithmetic operations to implement and proving the correctness of their hardware implementation is of great importance. In contrast to standard approaches that use satisfiability and equivalence checking techniques, the presented method verifies whether the gate-level square-root circuit actually performs a root operation, instead of checking equivalence with a reference design. The method extends the algebraic rewriting technique developed earlier for multipliers and introduces a novel technique of implicit hardware rewriting. The tool called SPEAR based on hardware rewriting enables the verification of a 256-bit gate-level square-root circuit with 0.26 million gates in under 18 minutes.

This paper addresses theoretical aspects of arithmetic circuit verification based on algebraic rewriting. Its goal is to advance the understanding of algebraic techniques for arithmetic circuit verification in the context of symbolic computer algebra. The paper offers a new insight into the arithmetic circuit verification problem, by viewing the computation performed by the circuit as the flow of digital data. In the proposed bit-flow model, the circuit is modeled as a network of logic components satisfying a bit-flow conservation law. We prove that the value of the flow of data in the circuit is invariant throughout the circuit and use this to prove soundness and completeness of the rewriting technique, independently from the computer algebra arguments. The efficiency of the method is illustrated with impressive results for large integer multipliers. The verification system and benchmarks are offered in an open source software environment.

This paper presents a fast and effective computer algebraic method for analyzing and verifying non-linear integer arithmetic circuits using a novel algebraic spectral model. It introduces a concept of algebraic spectrum, a numerical form of polynomial expression; it uses the distribution of coefficients of the monomials to determine the type of arithmetic function under verification. In contrast to previous works, the proof of functional correctness is achieved by computing an algebraic spectrum combined with local rewriting of word-level polynomials. The speedup is achieved by propagating coefficients through the circuit using And-Inverter Graph (AIG) datastructure. The effectiveness of the method is demonstrated with experiments including standard and Booth multipliers, and other synthesized non-linear arithmetic circuits up to 1024 bits containing over 12 million gates.

Division is one of the most complex arithmetic operations to implement and its hardware implementation requires thorough verification at the gate level. Dividers are difficult to verify using standard Boolean methods, such as equivalence checking or SAT-based techniques, as they require “bit-blasting” onto bit-level netlists. Other methods, such as theorem provers, concentrate mostly on proving correctness of the division algorithm. However, verification of low-level hardware implementations has received only a limited attention. This paper addresses the problem of verifying gate-level divider circuits by extending an algebraic model, successfully used to prove multipliers and other arithmetic circuits, to dividers. The method verifies whether the gate-level divider circuit actually performs a division, without a need for a reference design.

The paper presents a novel method to verify and debug gate-level arithmetic circuits implemented in Galois Field arithmetic. The method is based on forward reduction of the specification polynomials of the circuit in GF(2m) using GF(2) models of its logic gates. We define a forward variable order “FO >” and the rules of forward reduction that enable verification, bug detection, and automatic bug correction in the circuit. By analyzing the remainder generated by forward reduction, the method can determine whether the circuit is buggy, and finds the location and the type of the bug. The experiments performed on Mastrovito and Montgomery multipliers show that our debugging method is independent of the location of the bug(s) and the debugging time is comparable to the time needed to verify the bug-free circuit.

The paper describes a practical software tool for the verification of integer arithmetic circuits. It covers different types of integer multipliers, fused add-multiply circuits, and constant dividers - in general, circuits whose computation can be represented as a polynomial. The verification uses an algebraic model of the circuit and is accomplished by rewriting the polynomial of the binary encoding of the primary outputs (output signature), using the polynomial models of the logic gates, into a polynomial over the primary inputs (input signature). The resulting polynomial represents arithmetic function implemented by the circuit and hence can be used to extract functional specification from its gate-level implementation. The rewriting uses an efficient And-Inverter Graph (AIG) representation to enable extraction of the essential arithmetic components of the circuit. The tool is integrated with the popular ABC system. Its efficiency is illustrated with impressive results for integer multipliers, fused add-multiply circuits, and divide-by-constant circuits. The entire verification system is offered in an open source ABC environment together with an extensive set of benchmarks.