异步FIFO的模型检验方法

作     者：罗莉 欧国东 刘彬 徐炜遐 窦强 LUO Li;OU Guo-dong;LIU Bin;XU Wei-xia;DOU Qiang

作者机构：国防科技大学计算机学院长沙410073 

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

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2012年第39卷第3期

页      码：268-270页

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

主 题 词：CDC(Clock Domain Crossing) 异步FIFO LTL 符号模型检验 SMV 

学科分类：080903[080903] 0809[工学-计算机类] 08[工学] 

核心收录：

D　O　I：10.3969/j.issn.1002-137X.2012.03.061

馆 藏 号：203180488...