Effective Combination of Algebraic Techniques and Decision Diagrams to Formally Verify Large Arithmetic Circuits | IEEE Conference Publication | IEEE Xplore

Effective Combination of Algebraic Techniques and Decision Diagrams to Formally Verify Large Arithmetic Circuits


Abstract:

Arithmetic circuits require a verification process to prove that the gate level circuit is functionally equivalent to a high level specification. This paper presents an a...Show More

Abstract:

Arithmetic circuits require a verification process to prove that the gate level circuit is functionally equivalent to a high level specification. This paper presents an automatic equivalence checking technique to verify combinational arithmetic circuits at bit level. In order to efficiently verify gate level arithmetic circuits, we make use of computer algebra based approach so that the circuit and the specification are modeled in polynomial system and the verification problem is formulated as polynomial reduction techniques using Groebner basis of circuit polynomial corresponding ideal. To overcome costly Groebner basis computation as well as intensive polynomial reduction, we make use of a canonical decision diagram named Horner Expansion Diagram (HED), derive a suitable term order to represent and manipulate polynomials efficiently and find repetitive components based on automata. To evaluate the effectiveness of our verification technique, we have applied it to very large arithmetic circuits including multipliers. Preliminary experimental results show that the proposed verification technique is scalable enough so that large multipliers can efficiently be verified in reasonable run time and memory usage.
Date of Conference: 09-11 July 2014
Date Added to IEEE Xplore: 22 September 2014
ISBN Information:

ISSN Information:

Conference Location: Tampa, FL, USA

I. Introduction

Effort for verification of digital system designs grows as their size and complexity increase. In many practical designs such as Digital Signal Processing (DSP) for multimedia applications, arithmetic circuits are the main part of their datapaths. So verification of arithmetic circuits in a fast and precise way plays an important role in a digital system design flow. Several methods have been proposed to check an arithmetic circuit against its specification at a higher level of abstraction. Most of them are based on canonical graph-based representations like Binary Decision Diagrams (BDDs) that are not scalable because they suffer from space and time explosion problems when dealing with large arithmetic circuits especially multipliers [16] [17].

References

References is not available for this document.