Design And Implementation Of Verification Tool Based On Gr(?)bner Basis Method

The multiplier circuit is widely used and occupies an important position in the digital circuit system.But as the structure of the multiplier circuit becomes more and more complex,it brings a new challenge to the verification of the multiplier circuit.Errors can have serious consequences if they are not found in time.Therefore,the verification of multiplier circuits has become a crucial part in modern circuit design,and simulation and formal verification methods are the two main methods to verify multiplier circuits.Simulation is an engineering method that simulates the real behavior of electronic circuits by using mathematical models,but there are many fundamental problems in simulation that cannot be effectively solved.In order to solve such problems,the formal verification method has emerged as the times require,and it has become one of the most effective methods of multiplier circuit verification.In recent years,a variety of verification methods and optimizations of multiplier circuits have been developed.But these verification tools create redundancy in traversing the multiplier circuit nodes.When the polynomial is approximated,the verification efficiency will be slow due to the limitations of the algebraic computing system Mathematica or Singular.Verification failed and no corresponding attestation certificate was given.Based on the Gr(?)bner basis method,this thesis implements a verification tool in C++language,which includes four modules:parser,optimization strategy,polynomial solver and proof system.Each module can be easily integrated into other work.The parser includes reading the AIG file,and the optimization strategy uses sequential containers to store the nodes in each slice,reducing redundancy in the process of traversing nodes.The item can be represented as ordered linked lists of node variables,and the monomial contain a coefficient and an item.The polynomial library is established through an ordered linked list represented as a monomial.The polynomial solver is implemented to replace the previous algebraic computing system to reduce the canonical polynomial,which solves the problem of verification failure due to too many variables or too long computing time in the algebraic computing system to a certain extent.The experimental results show that the verification tool in this thesis not only does not stop the operation due to too many variables,but also improves the operation efficiency dozens of times,making it a powerful verification tool.In order to further enhance the reliability of the verification tool and ensure that there is no deviation in the verification process,this thesis adds the Nullstellensatz proof system to the verification tool.The proof system will generate gate constraints,cofactors,and gauge polynomials,which are the proof certificates.The verification process of the verification tool is said to be correct if the gate constraints are in turn multiplied by the auxiliary factors and added together to obtain the gauge polynomial.