Symbolic Model Checking of Asynchronous FIFO
Qiang Dou · 2012
Clock domain crossing(CDC) 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.