异步FIFO的模型检验方法

摘要：

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

关键词：CDC(Clock Domain Crossing)、异步FIFO、LTL、符号模型检验、SMV

所属期刊栏目：39

分类号：TN402(微电子学、集成电路（IC）)

资助基金：核高基重大专项2011ZX01028-001-001

在线出版日期：2012-05-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：268-270