Research On Formal Verification Method Based On I~2C Protocol

With the increasing scale and complexity of integrated circuits,the pressure of digital front-end verification is increasing.How to improve the efficiency of verification while ensuring the quality of verification is the key to solving this problem.At present,the most widely used verification method is dynamic simulation verification.Because the construction of the verification platform and the writing of incentives require a lot of manpower and time,and verification is difficult to cover all design scenarios,its application limitations are becoming increasingly prominent.Formal verification method is the method which uses mathematical methods to analyze the correctness of the design,The verification process does not require a verification platform,and can achieve full coverage verification,which is more complete and effective than dynamic simulation verification.This thesis is mainly about the research of formal verification methods.Based on the in-depth research of the principle and characteristics of formal verification,this thesis has completed the functional verification of I~2C-Master Core with formal verification method.In verification process,this thesis puts forward the verification efficiency strategy,complexity optimization method and verification quality measurement method.An automated verification platform based on formal verification is developed at the end.The main works of this thesis include:1.For the I~2C-Master Core of the design under test,the content of the I~2C standard protocol and the structure and function of design under test are analyzed.In the end,the extraction of the function points to be verified is completed.2.On the basis of formal verification research,a formal verification environment was built,a verification process was proposed,and all function points of DUT was verified.In the verification process,a verification strategy of segmented description property is used to improve verification efficiency,and the method of setting basic function coverpoints is used to ensure the correctness of verification.The verification results show that there are two corner error in the design,which proves the powerful bug hunting ability of formal verification.3.Aiming at the complexity problem of formal verification,three optimization methods are proposed based on the analysis of the complexity principle.In the process of DUT function verification,the application effects of the three optimization methods were compared and tested with the verification time and memory as the standard.The test results show that all three optimization methods can reduce the time and memory required for verification.4.Two coverage methods was used to measure verification quality,one is used to measure whether the attribute verification process has analyzed all possibilities,and the other is used to measure whether the current attribute list covers all design structures.In the end,the two coverage rates reached 99%and 100%respectively.5.Combining the above research results and actual project application scenarios,the development and testing of an automated platform based on formal verification have been completed.This platform can realize register read and write verification,register reset verification and connection verification.In this platform,you only need to fill in the verification function form according to the requirements,and the verification result will be automatically obtained.The correctness of the platform was verified through two sets of tests,and the results showed that the patform can get the verification results correctly and meet the design expectations.According to the research results,the formal verification method has the characteristics of high efficiency and accuracy,high coverage rate,and high bug capture ability.The automated verification platform based on formal verification also has the advantages of fast and accurate.In the follow-up work,we should continue to study the application effects of formal verification methods and their automation platforms in complex designs to promote the large-scale application of formal verification.