Design And Formal Verification Of Asynchronous FIFO

With the increasing of digital system size, a single clock domain design will greatly limit the digital system performance. To enhance the performance of modern digital systems, multiple clock domain design is conventionally adopted. While being transmitted, Cross-clock domain signals will come across the phenomenon of metastability, hence it will be a major concern for the multi-clock domain system designers to probe how to maintain the system stability and to have data transmission conducted smoothly. As to the bus system data transmission in the system where the two data interface clocks don't match, one of super and effective solutions is to use asynchronous FIFO buffer memory. How To solve the key and difficult issue that metastability and how to generate empty and full flag correctly in asynchronous FIFO design. Traditional FIFO design often synchronizes write/read address first, then compares them to generate empty/full signals. This design takes on too much area and can only work at a low frequency. A new method is proposed to overcome these problems.It optimizes gray code circuit to improve FIFO frequency,compares write/read address to generate full/empty flag first ,then synchronizes them to cut down quantity of synchronous registers. The results of FPGA verification and EDA synthesis both indicate that new asynchronous FIFO design has achieved a noticeable improvement.The design verification is traditionally fulfilled by simulation, however, with the increasing of circuit complexity, simulation takes a lot of CPU time, in practice, it is impossible to achieve exhaustive simulation to ensure the correctness of the design. To overcome the limitation of simulation, designers turned to a variety of formal verification methods, such as model checking, theorem proving and equivalence inspection and so forth. Using formal verification methods can guarantee the design correctness. This paper is to propose the asynchronous FIFO based on SMV model and utilize SMV symbolic model checking tools to verify the system model and the system attribute and achieve the desired results.According to the design and formal verification of asynchronous FIFO, we can effectively solve the metastable phenomenon generated during the transmission of cross-clock domain signal, effectively enhance the stability of digital systems and provide a reliable method for the validation of digital systems as well.