Multiplier Circuit Verification Based On Gr?bner Basis Method

Multiplier circuit,which plays an important role in digital signal field such as image processing and language encryption,is an indispensable part of complex chip system and integrated circuit.Multiplier verification is a difficult problem in VLSI design field.Traditional dynamic simulation and formal verification are both important verification methods of multiplier circuit.The advantages of dynamic simulation technology are simple operation and easy-to-understand principle,but it needs to select reasonable coverage for functional test of the circuit,which can not meet the verification requirements of large multiplier circuit.As a new and popular verification method,formal verification transforms the circuit verification problem into a mathematical problem and uses theoretical concepts,methods and tools to verify the correctness of the circuit.At present,the most concerned and effective method in fomal verification is the Gr?bner basis method.Bit-by-bit verification and adder rewriting are two important breakthroughs in Gr?bner basis method.Bit-by-bit verification slices the multiplier circuit according to the sum bit outputs,defines slicing Gr?bner basis for each slice,and then verifies the correctness of each slice by using ideal member algorithm.Using this strategy,the whole verification problem is decomposed into several sub-problems that can be easily solved to improve the verification efficiency.Adder rewriting is a key step in Gr?bner basis method,which can reduce the size of Gr?bner basis of the circuit and greatly speed up the reduction process of specification polynomial.However,there are still obvious deficiencies in these two optimization strategies.If bit-by-bit verification is combined with adder rewriting,then the time of adder rewriting is mainly used to the process of searching the adders.It is quite inefficient to search the adders by exhaustively traversing the gate variables in the circuit.If bit-by-bit verification is used alone,the verification time is mainly spent in the carry variables identifying algorithm.Influenced by traversal order and exhaustively traverse,the implementation of this algorithm has a lot of redundancy.Based on bit-by-bit verification and adder rewriting,this thesis proposes the following two optimizations: Firstly,a quick algorithm for searching all adders in circuit is presented in this thesis,which uses dynamic array to store the gate variables needed for searching adders,and searches adders according to inverse topological order.In this way,it can reduce redundant traversal greatly.Secondly,combined with the structural knowledge of multiplier circuit,the carry variables identifying algorithm is optimized according to the number of parent nodes of the variables in the AIG diagram of the circuit.The experimental results of these two optimizations show that the adder rewriting quick algorithm combined with dynamic array and the optimized carry variables identifying algorithm can improve the verification efficiency of the multiplier circuit by reducing redundant traversal.