异步FIFO的模型检验方法

• 作者: 刘彬 徐炜遐 欧国东 窦强 罗莉
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: CDC(Clock Domain Crossing) 异步FIFO LTL 符号模型检验 SMV
• 年，卷（期）: 2012,（3）
• 所属期刊栏目: 体系结构
• 页码范围: 268-270
• 分类号: TN402
• 字数: 2452字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2012.03.061

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗莉	国防科技大学计算机学院	26	233	7.0	15.0
2	徐炜遐	国防科技大学计算机学院	20	52	4.0	6.0
3	窦强	国防科技大学计算机学院	25	97	5.0	8.0
4	刘彬	国防科技大学计算机学院	8	9	2.0	2.0
5	欧国东	国防科技大学计算机学院	7	19	2.0	4.0