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 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.