异步FIFO的模型检验方法

Symbolic Model Checking of Asynchronous FIFO

跨时钟域(Clock Domain Crossing,CDC)设计和验证是SOC系统芯片设计的关键问题。讨论了异步FIFO的模型检验方法,利用模型检验工具SMV,建立了异步FIFO的有限状态机模型,使用时序逻辑LTL对该模型和属性进行了描述和验证。实验结果达到要求,同时表明该方法是行之有效的。与传统的模拟和仿真等验证方法相比较,模型检验具有能够自动进行、验证速度快、不用书写测试激励等优点。

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,