| In the past two years,European and American countries have tightened control over the integrated circuit industry,and chips have become a "stuck neck" problem.As a leader in independent innovation,China’s high-speed rail has already begun to tackle key problems in autonomous train control equipment and related technologies based on domestic chips.Facing such a huge distributed interactive system with complex functions,the system-level verification work after the localization of high-speed rail is also facing huge challenges.Against this background,this project takes the LEU in the high-speed rail system as the research object and combines the technology and methods of formal verification and simulation verification in the IC industry to conduct system-level verification on the key equipment replaced by the localization.This thesis extracts the model of the LEU system and designs four modules according to its functional structure,including FFFIS message coding module,RSSP-I protocol communication module,RS485 transmission module and DBPL coding module.The system white box is reshaped,which provides the system model and behavior expectations for the next step of the project testing work.By combining the two most important verification methods in the current verification field,the formal method and the UVM verification platform are used successively to verify the model based on the LEU system.Firstly,the function points that are not easy to be touched or require a large number of test vectors in the simulation are described in the form of assertions,and semi-formal verification is carried out by using formal tools,which can screen some key logic properties in the system design.Then the UVM platform is set up to carry out the universal constrained random excitation input.According to the actual situation,the normal operation and failure mode of the system are verified dynamically.After the establishment of the above verification platform,the coverage rate of formal verification was 100%,and the coverage rate of the UVM platform verification to the code reached 87.11%.The expected functions were realized.In formal verification,the formal tools based on assertions are mainly used to deal with the logic properties of combinatorial operations and the properties related to simple timing sequence in the design,including the parts with low coverage that are found after the verification of random excitation.In the UVM platform,the overall design is taken as a black box,and after a certain number of constrained random excitation inputs,the simulation results show that the expected functions of the LEU system design have been achieved successfully.Due to the functional structure and code style,the coverage of individual modules did not reach more than 90%.The uncovered codes were analyzed one by one and certain adjustments were made,which did not affect the functional verification of the design.By combining the completeness of formal method and the screening ability of simulation,the advantages were complemented,the coverage quality of the overall verification was improved,and the verification time was shortened.At the same time,the test vectors generated by the scientific method in the verification process of this thesis provide test case libraries for the subsequent test work. |
