Research And Application Of A Concise And Efficient Formal Verification Method

With the increasingly developing semiconductor technology,the chip integration has climbed to a higher and higher level.The growth in chip complexity will ultimately lead to an exponential increase in chip production costs,which means that the failure of the chip design will incur irreversible losses.Consequently,the verification of design quality has become more and more important,and effective chip verification methods have become the goal of the current industry.The traditional simulation verification methods,labor-intensive and time-consuming in writing verification incentives and building verification components,are no longer sufficient to meet the current verification needs.The formal verification method is attracting attention in the industry due to its potential to shorten project cycle and improve verification efficiency without the necessity of building simulation platforms or writing random incentives.When using formal verification methods,the excessive number of ports and registers of Design Under Test will lead to steep complexity,which can put a great strain on the computing power and memory and even give rise to the termination of the verification process.Therefore,the complexity problem is impeding the large-scale application of formal verification.How to optimize the complexity problem and efficiently use the formal verification method,while ensuring the quality of verification,has become the focus of engineering community.The main contents of this thesis are as follows:1.Through an analysis of the formal verification method,this thesis finds that formal verification engine,in the model phase,can introduce complexity into the state space by modeling all possibilities of Design Under Test,while introduce complexity in the analysis phase by analyzing the original input.Therefore,the key to solve the complexity problem is to reduce the number of states in the model phase and in the analysis phase respectively.2.To reduce formal verification complexity,this thesis proposes two methods,namely the black-box method and the cut-off method.The black-box method ignores modules that do not affect verification results in the model phase,so as to achieve the effect of reducing the state space.The cut-off method is a process in which the signal is cut off from the former logic and the analysis of the former signal driver ignored,so as to achieve the effect of reducing the state space.By applying both methods in the verification process of AXI2APB BRIDGE,the experimental results show that the black-box method can reduce the time loss by 18%-58% and the memory occupation by 24%-51% when verifying individual modules,and reduce time loss by 9%-10% and memory occupation by 15% when verifying multiple modules,while the cut-off method can reduce time loss by 32%-64% and memory occupation by 30%-68%.3.The functional verification of AXI2APB BRIDGE is achieved by an optimized verification methodology.In this thesis,the formal verification quality is measured by the state-space-based coverage rate and the property-based coverage rate,and the two formal verification coverage rates reach 99% and 100% respectively after the verification is completed.4.According to the scenario requirements of the actual project,a configurable formal verification flow,which can automatically complete register function check,register reset check,and inter-signal connectivity check,is designed.In the experiment,the availability of the process was checked by injecting an error into three checking items mentioned above in the experimental group respectively,meanwhile,the black-box method and the cut-off method are applied to the verification process to observe whether the two methods work or not.The experimental results show that the experimental group can report the errors in three types of checking items,in addition,the control group can correctly complete all three types of checking items.After using the cut-off method to verify the connectivity check and register function check,the verification time is reduced by 38% and 34%,and the memory occupation is reduced by 37% and 31%,while the verification time and memory occupation are reduced by 14% and 13% respectively after using the black-box method to verify the register reset check.