Design And Implementation Of The Integer Multiplier Verification Using Gr?bner Basis Method

Multiplier circuit is a basic part of modern digital circuit system,such as computer,signal processing,cryptography,AI equipment,etc.It is very important to verify its correctness.The traditional simulation technology and formal method are two kinds of verification methods of multiplier circuits.The traditional simulation technology has simple principle,strong operability and wide application range,but it can not meet the huge verification demand of current multiplier circuit design.Formal method has been widely accepted in recent years because of its short time consuming,low workload and more comprehensive characteristics.As one of the formal methods,Gr?bner basis method has attracted more and more attention and recognition in academic circles.At present,the mainstream method of integer multiplier verification is to first model it as an ideal member problem in commutative algebra,and then use the Gr?bner basis method in computer algebra systems such as Mathematica and Singular to determine.In order to further improve the efficiency of Gr?bner basis method,Ritirc et al.proposed bit-by-bit verification method.The idea of this method is to use the C language program to design the corresponding verification tool,and use the column item order to turn the circuit logic into slices,and through the verification tool to call the computer algebra system Mathematica and Singular to use the Gr?bner basis method to gradually verify the correctness of each slice of the circuit and then verify the correctness of the multiplier.Based on the research of Ritirc et al.,this paper carried out the following optimization:· Added a method to extract and combine gates,that is,find two types of gates in the slices.The first type is the logic gate which does not use the gate output to calculate the output value of the slice in which the gate is located,and this kind of logic gate is combined into the previous slice.The second type is the logic gate in the carry variable that depends on the other two logic gates in the carry variable,and we extract this logic gate into the next larger slice.By moving the above logic gate in the slice,the number of carry polynomial variables is reduced and the Gr?bner basis method is optimized.The experimental results show that the bit-by-bit verification algorithm with the gate extraction and combining method speeds up the verification efficiency.· The use of partial product elimination to reduce the circuit specification polynomials makes the polynomials more refined and improves the validation speed.· A new verification platform,Maple,a computer algebra system,has been added to this paper.A new implementation of the verification method is given by Maple,a computer algebra system,and a comparative experiment is carried out on computer.The experimental results show that the implementation of Maple has higher verification efficiency to some extent,and can be a powerful verification platform for integer multiplier.