Abstract: Clock domain crossing(CI}C) is an important issue in SoC design and verification. We presented the symbolic model checking of asynchronous FIFO, proposed a finite state machine to model the asynchronous FIFO, then, used SMV to analyze and check its specification described by linear temporal logic. Result shows the design is correct and the method is effective. Compared with simulation and emulation, model checking can save time, run automatically, and does not need test bench.

Key words: CI}C(Clock Domain Crossing) , Asynchronous FIFO, Linear temporal logic, Symbolic model checking, SMV