Application Of Formal Verification In Processor Verification

As the scale of embedded processors becomes larger and larger,its circuit logic becomes more and more complicated,and the difficulty of verification increases sharply.Traditional functional verification has the shortcomings of long verification cycle and incomplete verification.Traditional verification methods cannot meet the verification requirements of processor-scale circuits.Only by constantly updating verification techniques and building a diversified and multi-level verification framework can it be effective solve the current verification challenges.Formal verification is an emerging verification technology.On the basis of combining traditional functional verification,formal verification can fully consider the boundary conditions in the design.Therefore,studying the application of formal verification in processor verification has important reference value and application value for solving the problems in the current verification field.The verification object of this thesis is a certain RISC(Reduced Instruction Set Computer)processor core.Each module in the core integrates ECC(Error Correction Code)or EDC(Error Detection Code)safety modules.Because the safety module has a large input and output range under different configurations,there are many boundary conditions that are difficult to cover.Traditional verification methods requires resources to write test platforms and test cases.This thesis used formal verification methods to improve the verification efficiency of the modules in the core.First of all,based on the model checking method,this thesis extracted the characteristic attributes of the ECC and EDC modules and designed the assertion checking model.This thesis used the VC Formal tool to check the assertion attributes,and fully verified all the boundary conditions.The second,based on the equivalence check method,this thesis used sequential circuit equivalence check tools for all modules in the core that have added safety functions.This thesis proved that the functions of the modules in the core had not been changed after the safety functions was added.In addition,in order to verify whether the functions in the core meet the design specifications,this thesis adopted a coverage-driven verification method.First of all,a coverage model was designed for the key modules in the core.The second,a processor-level verification testbench was built according to the processor architecture.The testbench adopted the program of executing test instructions and running inspection.The testbench can monitor the key information in the core and compare it with the reference model.In addition,in order to efficiently generate test cases,this thesis also used a random instruction generator to write test cases and generate test files with random seeds.Finally,This thesis used random test cases for regression testing,and used the coverage analyzer in the VC Formal tool to perform coverage analysis on the design code.This thesis checked out some unreachable codes,and speeded up the progress of collecting coverage.The entire verification process fully combined the characteristics of formal verification and functional verification,and completed the verification of the processor efficiently in a short period of time.The results showed that the assertion properties of the two configurations of the ECC module passed the Formal check,and the running simulation time was 151.68 seconds in total.The assertion properties of a total of 128 configurations of the EDC module have all passed the Formal check,and the total simulation time was 8320 seconds.The sequential circuit equivalence check constraint input number was 778.Assertion output was 577.Total simulation time was 2641.08 seconds,and all 577 attributes are proved.The final code coverage rate reached 97.64%.The function coverage rate of each module reached 100%,These results have achieved the verification goal required by this thesis.