异步FIFO的设计与形式化验证
| 摘要 | 第1-10页 |
| ABSTRACT | 第10-11页 |
| 第一章 绪论 | 第11-17页 |
| ·研究背景与意义 | 第11-12页 |
| ·研究现状 | 第12-15页 |
| ·本文的主要工作 | 第15-16页 |
| ·论文结构 | 第16-17页 |
| 第二章 跨时钟域设计的挑战与实现方法 | 第17-32页 |
| ·跨时钟域设计的挑战 | 第17-20页 |
| ·亚稳态问题 | 第17-19页 |
| ·亚稳态产生的原因 | 第19页 |
| ·亚稳态的危害 | 第19-20页 |
| ·同步器的实现方法 | 第20-31页 |
| ·电平同步器 | 第24-25页 |
| ·边沿检测同步器 | 第25-26页 |
| ·脉冲同步器 | 第26-27页 |
| ·握手机制 | 第27-29页 |
| ·异步FIFO | 第29-31页 |
| ·本章小结 | 第31-32页 |
| 第三章 异步FIFO 的设计 | 第32-44页 |
| ·常见的异步FIFO 的设计 | 第32-35页 |
| ·改进的异步FIFO 的设计 | 第35-41页 |
| ·读写地址产生逻辑 | 第35-36页 |
| ·空/满标志的产生及代码的实现 | 第36-41页 |
| ·改进的异步FIFO 设计方法分析 | 第41页 |
| ·异步FIFO 的Verilog 实现与仿真 | 第41-43页 |
| ·异步FIFO 的FPGA 验证与DC 综合 | 第43页 |
| ·本章小结 | 第43-44页 |
| 第四章 异步FIFO 的形式化验证方法 | 第44-55页 |
| ·模拟验证与形式化验证 | 第45-46页 |
| ·定理证明 | 第46-47页 |
| ·等价性验证 | 第47-50页 |
| ·模型检验 | 第50-54页 |
| ·模型检验简介 | 第50-52页 |
| ·符号化模型检验 | 第52-53页 |
| ·模型检验工具 | 第53-54页 |
| ·本章小结 | 第54-55页 |
| 第五章 基于SMV 的异步FIFO 的模型检验 | 第55-68页 |
| ·符号模型检验系统SMV | 第55-61页 |
| ·SMV 系统相关概念 | 第56-58页 |
| ·SMV 语言介绍 | 第58-61页 |
| ·基于SMV 的异步FIFO 验证步骤 | 第61页 |
| ·异步FIFO 的有限状态机模型 | 第61-63页 |
| ·异步FIFO 属性的LTL 描述 | 第63-64页 |
| ·实验结果 | 第64-67页 |
| ·实验环境 | 第64页 |
| ·SMV 模型检验结果 | 第64-67页 |
| ·实验结果分析 | 第67页 |
| ·结论 | 第67-68页 |
| 第六章 结束语 | 第68-69页 |
| 致谢 | 第69-70页 |
| 参考文献 | 第70-75页 |
| 作者在学期间取得的学术成果 | 第75页 |
