Equivalence Verification Of Integer Multipliers Based On Gr?bner Basis Method

With the rapid development of science and technology,digital systems have been widely used in cryptography,Automated theorem proving,communication protocols and other fields.The perfection of large scale integrated circuit(LSI)has led to the increasing proportion of multiplier circuit in modern computer system,so it is very important to verify the multiplier circuit integrated circuit design.The traditional verification method is the simulation technology,its biggest advantage is simple operation,low limitations,and the principle is easy to understand.It is effective for the verification of small circuits,but it is difficult to meet the verification requirements for the complex and large scale multiplier circuits.In order to solve such problems,formal verification,which has the unique advantages of completeness and automation,comes into being.Equivalence checking is one of the formal verification methods,which verifies the functional consistency of the two design models: formal design and implementation.The equivalence checking of multipliers has been a difficult problem in the field of large-scale Arithmetic integrated circuit design.At present,the most effective way to solve the problem of Integer multiplier arithmetic circuit verification is the symbol based computer algebra system technology.Polynomial as an abstract symbol in algebra,is an ideal tool for circuit modeling because of its strong abstract modeling ability,normative and unambiguous representation when describing circuits.Based on this,this thesis uses the one-to-one correspondence between logic gate and polynomial to construct the Gr?bner basis algebraic model of integer multiplier.The integer multiplier equivalence verification problem is transformed into the ideal member determination problem,and then the Gr?bner basis method is used to verify the problem in the computer algebra system.This paper presents a new method for incremental verification of integer multiplier structure after bitwise slicing.A comparative experiment on Mathematica,a computer algebra system in Linux platform shows that: This method can not only detect errors in integer multiplier circuits up to 128-bit,but also has higher verification efficiency compared with Lingeling,ABC and incremental methods.