学海网

毕业设计-空间总线通信系统关键模块模拟与验证—模拟与形式验证分析，共71页，23654字，附开题报告等
主要内容
空间总线通信系统关键模块模拟与验证
第一部分：用Mentor公司的Questa工具分别对关键模块（包括发送模块、接收模块和控制模块）进行模拟仿真。第一步：先阅读关键模块的设计规范，了解什么需要验证，并且制定一个关于该模块的验证计划。第二步：创建该模块的测试环境（包括输入激励模块、待测设计模块和收集验证结果模块），输入激励模块主要负责输入适当的激励，完成其他模块的调用等。待测设计模块就是要进行模拟仿真的模块，设计人员设计的程序。收集验证结果模块主要包括断言、收集覆盖率等。第三步：输入激励，观察模拟仿真的结果。如果出现断言失败的话，分析失败的原因：首先检查是不是断言写的与设计规范要求有出入。其次，如果前一步确认无误的话，就很有可能是待测设计出错了，这正是我们想要看到的结果。观察仿真波形，看看断言是如何失败的，然后去找到相应代码的区域，分析出错的位置。
第二部分：用NuSMV模型检测工具分别对关键模块（包括控制模块、发送模块和接收模块）验证。第一步：先阅读关键模块的设计规范，了解什么才是想要出现的行为，并且制定一个关于该模块的验证计划。第二步：创建该模块的模型，写出待测的性质（就是要验证的功能）。这个模型主要包括两部分：一部分是状态转移的模型，另一部分是待测性质。跟模拟最终要的区别在于它不需要关注输入激励。第三步：利用工具检测模型，观察验证结果。这个工具的一个好处就是性质不总是真的话，总会给出一个反例的。根据反例找出是性质的原因还是模型不准确。
第三部分：如果时间充足的话，用Questa工具对控制模块、发送模块和接收模块进行组合验证。不用NuSMV的原因是三个模块组合验证的话模型很大，可能会发生状态爆炸。
第四部分：总结模拟与验证的成果，得出相应的结论：模块是否有错误。

摘要
空间总线（SpaceWire）协议是应用于航空航天领域的高速通信总线协议，对SpaceWire系统设计正确性要求很高，因此对SpaceWire系统的严格验证一直是备受关注的问题之一。虽然形式化验证能解决传统验证方法存在的不完备性的问题，但是它也存在由原来设计到系统形式建模的抽象精度问题。为了解决上述这个问题，本文采用对其进行模拟与形式化验证相结合的方式来保证系统设计和实现的功能正确性和可靠性。一方面，使用NuSMV形式化验证工具对SpaceWire关键模块的设计进行形式验证，保证验证完备性的需要；另一方面， 基于Questasim模拟仿真工具对设计进行模拟验证。因此，通过形式断言将模拟与形式验证紧密地联系在一起。模拟可更大程度地缩小了抽象的形式模型与被验证模块的设计差距，形式验证保证了完备性的要求。将模拟与形式验证相互结合，取其所长，来确保SpaceWire通信系统满足协议规范的要求。
关键词：形式化验证；模拟；SpaceWire标准；断言

Abstract
SpaceWire protocol is applied in the field of aerospace high-speed communication bus protocol. It requires extremely high correctness on the SpaceWire system design ,so strict validation on the SpaceWire system has always been one of the problems that concern. Although formal verification can solve the problem of incompleteness existing in traditional verification methods , it also exists a conversion accuracy problem from the original design to system model. In order to solve the above problems, this paper adopts the way of combining simulation with formal verification to ensure the correctness and reliability of SpaceWire system. On the one hand, we use formal validation tool called NuSMV to do form verification on the system to ensure the completeness of the requirements; On the other hand, we use simulation tools called Questasim to simulate the system. Simulation and formal verification are closely linked by means of the formal assertion. Simulation will further close the gap between the formal model and the design and form validation will ensure the requirements of the completeness. Combination simulation with formal verification and taking their strong points ensure that the SpaceWire communication system to meet the requirements of the protocol specification.
Key words:formal verification; simulation; SpaceWire standards; assertions　

目录
第一章 引言 7
第二章 模拟与形式化验证的理论 8
2.1形式化验证的理论知识 8
2.1.1形式化验证技术 8
2.1.2基于模型检测处理的验证方法 8
2.1.3模型检测 8
2.1.4线性时态逻辑（LTL） 8
2.1.5 分支时间逻辑（CTL） 10
2.1.6模型检测算法 11
2.2 模拟的理论知识 12
2.2.1约束随机激励测试 12
2.2.2断言验证 12
2.2.3覆盖率驱动的验证 13
2.3形式验证的流程 14
2.4 模拟的流程 14
第三章 发送模块验证 16
3.1发送模块简介 16
3.2 发送子模块性质验证 18
3.2.1字符数据发送控制子模块性质验证 18
3.2.2 字符数据寄存器子模块性质验证 20
3.2.3 时间码发送控制子模块性质验证 22
3.2.4 时间码寄存器子模块性质验证 22
3.2.5发送控制子模块性质验证 24
3.2.6发送寄存器子模块性质验证 26
3.3发送子模块断言验证 27
3.3.1字符数据发送控制子模块断言验证 27
3.3.2字符数据寄存器子模块断言验证 29
3.3.3时间码发送控制子模块断言验证 32
3.3.4时间码寄存器子模块断言验证 32
3.3.5发送控制子模块断言验证 33
3.3.6发送寄存器子模块断言验证 35
3.4 发送模块的形式验证与模拟结果与分析 37
第四章 接收模块验证 39
4.1 接收模块简介 39
4.2 接收模块性质验证 41
4.3 接收模块断言验证 42
4.4 接收模块的形式验证与模拟结果与分析 45
第五章 控制模块验证 46
5.1 控制模块简介 46
5.2 控制模块性质验证 49
5.3 控制模块断言验证 55
5.4 控制模块形式验证与模拟结果与分析 61
第六章 多个模块综合验证 63
6.1 定时器复位的验证 63
6.2 控制模块状态机的验证 66
6.3 控制字符发送和接收的验证 67
6.4 多模块模拟验证分析 68
第七章 结论和建议 70
7.1 结论 70
7.2 设想与建议 70
参考文献 71