Design And Formal Verification Of Asynchronous_FIFO Based On SOC

In recent years, with the rapid development of IC industry, semiconductor technology level has reached submicron, it caused the status quo of chip integration scale more and more complex. Throughout the chip design process, from behavioral level HDL to the last stage, the most complex and the most important link is the verification. In the face of greater validation pressure, traditional simulation validation have been gradually exposed its limitations. Formal verification method is used to supply the traditional verification method, increasingly aroused people’s concern. Formal verification method has different validation logic to accomplish validation goals, can overcome shortcomings of traditional verification method, so this thesis? research center is formal verification method, and combined with Jasper platform proposed the new formal verification method that has greater applicability.First of all, this thesis selects the asynchronous FIFO which is commonly used in SOC to be a test object. Based on the design structure and function implementation logic of traditional asynchronous FIFO, the improved design of asynchronous FIFO in this thesis is put forward. Compared with the traditional design, the improved design?s advantage is using the new empty and full flag judgment logic, and overcomes the limitation of traditional memory in the depth of RAM. The second, this thesis analyzes the current application of limitations of formal verification, studied the logic principle of formal verification method based on Jasper platform and significance of formal verification state space, and made a detailed explanation about the process of Jasper formal verification, at the same time, introduces the characteristics of Jasper validation language SVA, SVA language is studied through example analysis on how to descript design features. Finally, to verify improved asynchronous FIFO, the thesis made a specific validation plan and finished the writing of assertion based on functions structure of the asynchronous FIFO design early. In the analysis of verification results, the thesis discussed in detail how to use the Jasper graphical interface to debug by giving an example.The research results show the formal verification method based on Jasper platform has alot of advantages compared with the traditional simulation verification method, it do not need to write Testbench or Testcase, has shorter verification cycle, high test coverage, etc.At present, the formal module checking method this thesis studied has been widely used in the INTEL SOC verification project. It is usually used with simulation method, greatly improving the efficiency of the original single verification method. The research of Formal verification methods has far-reaching practical significance on the development of future digital IC verification, at the same time, also offers a full verification guarantee for the increasingly complex digital IC design.