| WISHBONE片上总线符号模型检测 |
| |
| 引用本文： | 逄涛,段振华.WISHBONE片上总线符号模型检测[J].计算机研究与发展,2014(12). |
| |
| 作者姓名： | 逄涛 段振华 |
| |
| 作者单位： | 西安电子科技大学计算理论与技术研究所; |
| |
| 基金项目： | 国家“九七三”重点基础研究发展计划基金项目(2010CB328102);国家自然科学基金项目(61003078,61272117,61133001,61272118,91218301,61322202,61202038) |
| |
| 摘 要： | 随着多核体系结构的出现和普及,片上总线逐渐成为影响片上系统功能和性能的关键部件.因此,片上总线的验证成为片上系统设计中一个重要组成部分.模型检测作为一种主流的形式化验证方法,可以自动化穷举搜索系统行为以决定片上系统的设计是否满足设计规范.然而,模型检测受制于状态空间爆炸问题,且现有规范语言如计算树逻辑和线性时序逻辑等的描述能力有限.提出了一种基于命题投影时序逻辑的WISHBONE片上总线符号模型检测方法.该方法将以Verilog硬件描述语言实现的WISHBONE总线转化为以NuSMV模型检测工具的建模语言SMV描述的系统模型,使用命题投影时序逻辑描述WISHBONE总线期望的性质,通过PLSMC工具验证系统模型是否满足期望的性质.实验结果表明该方法能够有效验证WISHBONE片上总线的定性性质,以及时间敏感和迭代性等定量性质.
|
| 关 键 词： | 时序逻辑 符号模型检测 WISHBONE总线 片上系统 形式化验证 |
| 本文献已被 CNKI 等数据库收录！ |
|
