Functional Verification And Formal Verification Optimization Of Processor Safety Features

With the gradual electronization and intellectualization of the automotive industry,the failure of any on-board chip can lead to serious safety accidents,and the safety requirements of automotive chips are also increasing.Processor chip is necessary for automotive electronic system.The functional verification of the safety features of vehicle processor chip is an important link to ensure the safety of automotive electronic system.Traditional simulation verification methods have some disadvantages,such as long verification time,complex testbench and difficult to find corner case.Simulation verification methods alone have been difficult to meet the verification requirements of processor safety features.The formal verification method has the advantages of high efficiency,ease of use and completeness,and can better solve the problems in safety features’ functional verification.On the basis of traditional simulation verification,exploring the application method and practical effect of formal verification method in processor safety features’ functional verification is of great significance to improve the efficiency and quality of verification.This paper verifies the safety features of RISC dual-core processor based on ISO26262 standard.First,the simulation verification method is applied to complete all the functional verification,and then the formal verification method is applied as the optimization method to verify some modules.This paper verifies the correctness of the lockstep design,safety access function,safety bus function and safety register of the safety features of the processor.Based on the simulation verification method,,the following work is completed:(1)In order to verify the lockstep error detection function,build the testbench error injection environment,simulate external interference errors,realize reasonable error injection and result inspection under the complex and diverse conditions of injection point,injection time and error types,and verify the correctness of error detection function and relevant safety registers.(2)In order to verify the safety access function of processor designed based on DualCore Lockstep principle in the safety system.In the case of safety master / slave devices,the corresponding safety access function verification environment has been established respectively,and the safety bus and safety register have been verified.(3)For the 12 main verification aspects,13 test cases are written to generate processor instruction sequences according to different strategies.Establish the coverage model,realize8 functional coverage groups,and collect the relevant coverage of lockstep design function,security bus function,security monitor function,safety access function and groups of safety registers.All test cases run through.After a large number of regression tests and excluding the correct inaccessibility,the final code coverage and function coverage reach 100%,meeting the requirements for verifying the project coverage.Based on the formal verification method,the following work is completed:(1)Build the basic running environment of VC formal,and apply formal property verification(FPV)to verify the function of safety bus with 27 properties.(2)Using register formal verification(FRV)and security register IP-XACT,201 properties are checked to verify the property of safety register.(3)The formal coverage analyzer(FCA)is executed to analyze the coverage of the simulated original coverage data to accelerate the coverage convergence.(4)Build an automatic formal verification environment to improve the efficiency of formal verification,realize automatic disassembly of modules and submit formal verification analysis tasks.,and reduce the more time-consuming formal verification analysis running time by more than 90%.All properties checked for formal validation passed.After formal coverage analysis,the overall coverage increased from 68.45% to 70.57%,and the coverage of some modules increased by more than 15%.In this paper,the simulation verification method is adopted to verify the safety features and functions of RISC dual-core processor based on ISO26262 standard,and the formal verification method is applied for verification and optimization.Under the condition of limiting the design module,compared with the simulation verification,the verification running time is reduced by about 90%,the space occupation is reduced by about 75%,the workload required for verification such as coverage collection is reduced by more than 30%,and some corner cases are found and solved.