Groebner basis based formal verification of large arithmetic circuits using Gaussian elimination and cone-based polynomial extraction

Abstract

Verification of arithmetic circuits is essential as they form the main part of many practical designs such as signal processing and multimedia applications. In these applications, the size of the datapath could be very large so that contemporary verification methods would be almost incapable of verifying such circuits in reasonable time and memory usage. This paper addresses formal verification of large integer arithmetic circuits using symbolic computer algebra techniques. In order to efficiently verify gate level arithmetic circuits, we model the circuit and the specification with polynomial system and the verification problem is formulated as membership testing of the given specification polynomial in corresponding ideal of the circuit polynomials. The membership testing needs Groebner basis reduction. In order to overcome the intensive polynomial reduction needed in Groebner basis computation so that we can deal with verifying large arithmetic circuits, the fanout-free regions (cones) of the circuit are extracted and represented as corresponding polynomials automatically. For further improvement, we make use of Gaussian elimination concept to perform specification polynomial reduction w.r.t Groebner basis using a matrix representation of the problem. To evaluate the effectiveness of our verification technique, we have applied it to very large arithmetic circuits with different architectures. The experimental results show that the proposed verification technique is scalable enough so that large arithmetic circuits can efficiently be verified in reasonable run time and memory usage.

Introduction

As the size and complexity of digital systems increase continuously, design verification and debug are quickly becoming more important. From a verification point of view, one of the most difficult parts in complicated digital designs is arithmetic datapaths and their components, such as multipliers and dividers. Arithmetic circuits are the main part in many computational intensive designs, e.g. Digital Signal Processing (DSP) units in multimedia applications. The complicated and specialized nature of these arithmetic architectures requires custom design which makes the implementation error-prone. Therefore, verification of arithmetic circuits in a fast and precise way plays an important role in a digital system design flow.

Formal verification methods make use of mathematical techniques to insure the integrity of a design with respect to some desired characteristics. Several formal methods have been proposed to verify the correctness of arithmetic circuits in higher level of abstraction. Most of them are based on canonical graph-based representations like Binary Decision Diagrams (BDDs), which are not scalable because they suffer from space and time explosion problems when dealing with large arithmetic circuits especially multipliers [16], [17].

On the other hand, recently some techniques for verification of bit-level implementations using the theory of Groebner basis have been proposed [6], [7], [9]. However, these techniques are computationally intensive and are not scalable to large arithmetic circuits.

Addressing the above problems, this paper proposes a formal verification technique to verify gate level circuits that implement integer arithmetic circuits so that their specifications are given as polynomial functions f_spec. The goal of the verifier is to guarantee the equivalence of f_spec and gate level implementation f_imp. In fact our proposed method uses Groebner basis theory to effectively verify large arithmetic circuits. This theory enables us to formulate the verification problem as an ideal membership testing. Fig. 1 shows our proposed verification technique which takes a gate level circuit (f_imp) and its high level specification (f_spec) as inputs. In order to check whether f_imp is functionally equivalent to f_spec or not, first of all, the gate level circuit is converted to Boolean polynomials by extraction of fanout free regions (which are referred to as cones) and mapping cones to polynomials. We automatically exploit the cones in order to achieve a smaller number of circuit polynomials. We will discuss how to find them based on a backtracking algorithm and obtaining their equivalent polynomials in Section 4. As we will see in Section 3, the ideal membership testing requires Groebner basis computation which is computationally extensive. In order to remove the need of this computation, a topological order of polynomials’ variables (eke polynomials’ terms) is utilized in Section 4. This ordering eliminates the computation of Groebner basis as well as making the initial set of the circuit polynomials (F) Groebner basis itself. Then the equivalence checking is performed by polynomial manipulation and reduction of the specification polynomial (f_spec) over Groebner basis polynomials (F) [10]. We call this step Groebner basis reduction or polynomial reduction.

As will be discussed in Section 3, the mathematical manipulations (Groebner basis reduction) contain polynomial divisions and multiplications which are complicated in terms of run time and memory usage as the intermediate polynomials may become very large. In order to overcome these intensive computations, we utilize the modification of F4 algorithm [24] for computing Groebner basis reduction on a matrix which represents the verification problem. By using this method, we will be able to verify large arithmetic circuits in reasonable run time and memory space usage as experimentally shown in Section 6. In summary, our contributions in this work are as follows:

• Extracting a finite set of Boolean polynomials from the gate level implementation by looking for fanout free regions (cones). In contrast to [18], [19], [20], this method is applicable even when half adder and full adders cannot be extracted due to the local optimizations which are usually done by synthesis tools (Section 4).

• In contrast to [29] in which we looked only for repetitive components (which needs some information about repetitive components provided as a library), the proposed method in this work enables us to reduce the number of polynomials significantly so that the verification time decreases dramatically while we do not have any information about the repetitive components.

• Determining a suitable variable ordering for cones’ polynomials in such a way that the leading terms of the circuit polynomials become relatively prime to avoid Groebner basis computation (Sections 3 Preliminaries, 4 Proposed verification technique).

• Improving F4 algorithm and using Gaussian elimination to perform polynomial reduction efficiently so that a sequence of polynomial divisions can be efficiently computed (Section 5).

The paper is organized as follows: Section 2 provides a brief review of related work. In Section 3 we briefly describe some mathematical background as well as Horner Expansion Diagrams (HEDs) [14], [15]. Section 4 presents our proposed verification technique in detail. Section 5 describes our approach to use Gaussian elimination in order to perform the Groebner basis reductions. The experimental results are shown in Section 6 and Finally, Section 7 concludes the paper.