Analysis And Research Of Logical Equivalence In Digital LTE Chip Based On Formal Verification

Throughout the whole IC design process,from the initial design of the chip architecture to the final tape-out,verification is the most important and time costing aspect of the processing.In terms of the design with nano-level scale,the traditional dynamic verification methods have not been able to complete the task of the whole verification work.The formal verification method has a good integrality of the verification coverage,and it is very suitable for the implementation in large-scale design.Therefore,formal verification is becoming widely used by industry.How to analyze the failures of the formal verification,locate the problems with speed and accuracy,and provide a feasible solution,has become a main focus in the engineering field.This thesis is based on comprehensively summarize on the current research of formal verification technology which is widely used in IC backend field.Combined with author's own experience during the internship in the LTE chip project,the logic equivalence comparison is analyzed and obtained with satisfied results in practical engineering project.This thesis contains the following works:Firstly,the verification process of the digital LTE chip is divided into five steps by this thesis: environment setup,initializing,read in files or constraints,set options and comparison.In this way,the range of the follow-up analysis and debugging work could be more clear and accurate.Combined with the commands of the LEC tool to carry on the operation run-script standard,define each necessary command and its options in the process.Based on the comparison between flatten and hierarchical methods of logical equivalence check,the respective principles,implementation methods and characteristics are analyzed.Secondly,in the aspect of the logical equivalence comparison,this thesis establishes the debugging idea of the flatten mode according to its principle and characteristics.Then this thesis discusses several problems that may cause the failure of the formal verification,and puts forward the solution to these problems.The results show that the main reasons of the failure are: file missing,name error,scan signal participation logic,UPF problem,and design or synthesis problem.The first three problems can be solved by debugging during the formal verification,but the latter two need the cooperation with the designers.Thirdly,according to the principle and characteristics of the hierarchical model,the debugging method of the model is defined.On this basis,because of the characteristics of large scale and complex structure in the hierarchical mode,this thesis analyzes the reasons for the failure of the two kinds of special verification,and proposes their solution.The results show that there are two problems named Design Ware problem and uniquify problem,which due to the complex structure of the verification object.These can be solved by pre-read interrelated files and add special constraints.At last,in order to solve the problem of low efficiency and long time in dealing with a large number of aborts in the flatten comparison,an improved method named isolation comparison is proposed.This method combines the traditional solve aborts methods which are based on tool commands,using hierarchical mode of high efficiency aborts problem.The isolation comparison can concentrate abort points in internal sub module of the design,so as to shorten the run-time to improve the verification efficiency.