Optimization And Implementation Of Gr(?)bner Basis Method Based On Hash Table

At present,the circuit is an important component in the field of Very Large Scale Integration design and chip research and development of electronic products.In circuit verification,verification multiplier time accounts for up to 70%,so the importance of multiplier circuit verification is self-evident.In the field of multiplier circuit verification,simulation technology and formal method are two kinds of verification methods.The simulation technology has the characteristics of wide application range and easy to understand principle,but in the aspect of circuit verification,it needs appropriate coverage for testing,which is time-consuming and inefficient.The formal method is to use mathematical methods to prove that the circuit satisfies the given design specification.Among the formal methods,SAT method,decision graph method,theorem proving method,bit-level reverse engineering method and Gr(?)bner basis method can verify the simple circuit.Among them,the most suitable formalization method is Gr(?)bner basis method.The essence of Gr(?)bner basis method is to turn the verification problem of multiplier circuit into the membership problem of ideal members,improve the operability of the experiment and complete automation of the verification process,reduce the verification cost and reduce the difficulty of the verification.On this basis,Ritirc and his research team made further achievements,and proposed the method of rewriting the adder to simplify the Gr(?)bner basis.However,the number of variables that need to be traversed by this method increases exponentially,and it relies too much on carry variables when identifying the adder,which leads to more memory and time consumption in the verification process.Therefore,this thesis focuses on the optimization of the adder rewrite method,and then proposes an adder rewrite optimization algorithm based on hash table.With the advantage of data structure of hash table,the algorithm uses it to store the variables required in the multiplier circuit,and the number of variables in the traversal is reduced.Get rid of carry variables,choose to use the structural characteristics of the adder to complete the identification,and finally reduce the memory usage,optimize the algorithm structure,improve the verification efficiency.In order to make the algorithm operable,the optimization algorithm is implemented in this thesis,and the comparison experiment is carried out with the original method of rewriting the additive.Finally,considering the theoretical and experimental results,it can be shown that the optimization algorithm can improve the verification efficiency of the multiplier circuit,reduce the time cost and memory occupation.