Formal Verification Of The Vector Integer Arithmetic Logic Unit

With the increasing complexity and difficulty of integrated circuit design,verification is a core part of the design process,faced with great challenges.According to statistics,more than 50 percent of the human resources and time are put into the verification work of the chip design,therefore,it's important to improve the efficiency and integrity of verification for integrated circuit design and development.The traditional simulation verification is considerably dependent on the completeness of the test case.Obviously,when the traditional method faces with large-scale design,it gradually exposes the limitation which is difficult to cover all the test case.In recent years,as a supplement to simulation verification,formal verification has received wide attention from the industry because itcan traverse the entire state space by an efficient approach and test and verify the design completely.Formal verification in connection with VIALU(Vector Integer Arithmetic Logic Unit)of server processor core is studied in our research work.Using Jasper Gold and ATEC formal verification tool,we have completed the functional verification for the VIALU by equivalence checking.The main work of the thesis can be listed as follows.First,according to the design specification of the VIALU,we complete the design and test of the reference model.We analyze the functions of 138 instructions,including vector integer instructions and a small number of floating-point instructions.After that,the reference model that required for formal verification is programed by the C language.In order to ensure the validity of the reference model,We verify the functional consistency of model and design specifications with a combination of directional and random testing.Second,According to the VIALU,we study the formal verification technique based on equivalence checking to solve the problem of the inadequacy of formal verification capability.First of all,considering the size of the VIALU and the characteristics of the circuit structure,we propose a reasonable verification scheme.Then,for the key sub-modules in the design,the Verilog HDL language is used to describe its circuit functions and SEC(Sequential Equivalence Checking)of Jasper Gold is used to verify its key function.Finally,for the entire ALU,we verify the consistency of circuit design and reference model by the ATEC tool.In the early stages of verification,in order to quickly locate the design defects,we verify the correctness of the instruction function one by one by excessive signal constraint.After the design scheme tends to be stable,the excessive signal constraint in the formal verification is removed and the complete functional verification is realized.Compared with the simulation verification method,the formal verification can find the counter example quickly without constructing a complex verification platform and generating a large number of test cases,and especially in the scenario of random testing which is difficult to cover corner case.Therefore,the formal verification method has a great advantage in ensuring the completeness and improving the efficiency.The test results show that the solution of effective Case-Splitting by over-constrained to the contradiction between the design scale and the formal verification capability is feasible.This solution can provide a reference for the verification of other processors computing units.