异步FIFO的设计与形式化验证

论文摘要

随着数字系统规模的不断增大,单时钟域设计会极大地限制数字系统性能,现代数字系统为了提升性能,常采用多时钟域的设计。跨时钟域的信号在传输时会遇到亚稳态现象,如何保持系统稳定地传输数据是多时钟域系统设计者重点关注的问题,异步FIFO是一种优秀和有效的解决方案。如何避免亚稳态现象及空满控制信号的产生是异步FIFO设计的难点问题,常见的异步FIFO设计采用先同步读写指针后比较产生空满标志的方法,工作频率低,面积大,本文提出了一种新型异步FIFO的设计方法,优化了以格雷码编码的电路,提高异步FIFO的工作频率,用先比较读写指针产生空满标志,再同步到相应时钟域的方法,避免使用大量的同步寄存器,减少了面积空间。FPGA验证及EDA综合的结果表明,改进后的异步FIFO性能有了显著的提高。传统设计的验证是通过模拟验证来完成的,然而随着电路复杂性的日益增加,模拟验证需要开销大量的CPU时间,并且穷举的模拟验证很难保证设计的正确性。为了克服模拟验证的局限性,设计者求助于各种形式化的验证方法,如模型检验、定理证明和等价性检验等,使用形式化验证方法可以有效地保证设计的正确性。本文提出了一种基于SMV的异步FIFO的模型检验方法,利用符号化模型检验工具SMV对该系统模型和系统属性进行了验证,达到了预期的效果。通过异步FIFO的设计和形式化验证,可以有效地解决跨时钟域信号传输产生的亚稳态问题,有效地提升了数字系统的稳定性,同时也为数字系统的验证提供了一种可靠的方法。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 研究背景与意义
• 1.2 研究现状
• 1.3 本文的主要工作
• 1.4 论文结构
• 第二章 跨时钟域设计的挑战与实现方法
• 2.1 跨时钟域设计的挑战
• 2.1.1 亚稳态问题
• 2.1.2 亚稳态产生的原因
• 2.1.3 亚稳态的危害
• 2.2 同步器的实现方法
• 2.2.1 电平同步器
• 2.2.2 边沿检测同步器
• 2.2.3 脉冲同步器
• 2.2.4 握手机制
• 2.2.5 异步FIFO
• 2.3 本章小结
• 第三章 异步FIFO 的设计
• 3.1 常见的异步FIFO 的设计
• 3.2 改进的异步FIFO 的设计
• 3.2.1 读写地址产生逻辑
• 3.2.2 空/满标志的产生及代码的实现
• 3.2.3 改进的异步FIFO 设计方法分析
• 3.3 异步FIFO 的Verilog 实现与仿真
• 3.4 异步FIFO 的FPGA 验证与DC 综合
• 3.5 本章小结
• 第四章 异步FIFO 的形式化验证方法
• 4.1 模拟验证与形式化验证
• 4.2 定理证明
• 4.3 等价性验证
• 4.4 模型检验
• 4.4.1 模型检验简介
• 4.4.2 符号化模型检验
• 4.4.3 模型检验工具
• 4.5 本章小结
• 第五章 基于SMV 的异步FIFO 的模型检验
• 5.1 符号模型检验系统SMV
• 5.1.1 SMV 系统相关概念
• 5.1.2 SMV 语言介绍
• 5.1.3 基于SMV 的异步FIFO 验证步骤
• 5.2 异步FIFO 的有限状态机模型
• 5.3 异步FIFO 属性的LTL 描述
• 5.4 实验结果
• 5.4.1 实验环境
• 5.4.2 SMV 模型检验结果
• 5.4.3 实验结果分析
• 5.5 结论
• 第六章 结束语
• 致谢
• 参考文献
• 作者在学期间取得的学术成果