WISHBONE片上总线符号模型检测

发布时间：2019-02-18 07:37

【摘要】：随着多核体系结构的出现和普及,片上总线逐渐成为影响片上系统功能和性能的关键部件.因此,片上总线的验证成为片上系统设计中一个重要组成部分.模型检测作为一种主流的形式化验证方法,可以自动化穷举搜索系统行为以决定片上系统的设计是否满足设计规范.然而,模型检测受制于状态空间爆炸问题,且现有规范语言如计算树逻辑和线性时序逻辑等的描述能力有限.提出了一种基于命题投影时序逻辑的WISHBONE片上总线符号模型检测方法.该方法将以Verilog硬件描述语言实现的WISHBONE总线转化为以NuSMV模型检测工具的建模语言SMV描述的系统模型,使用命题投影时序逻辑描述WISHBONE总线期望的性质,通过PLSMC工具验证系统模型是否满足期望的性质.实验结果表明该方法能够有效验证WISHBONE片上总线的定性性质,以及时间敏感和迭代性等定量性质.
[Abstract]:With the emergence and popularization of multi-core architecture, on-chip bus has become a key component affecting the function and performance of on-chip system. Therefore, the verification of on-chip bus becomes an important part in the design of on-chip system. As a mainstream formal verification method, model checking can automate the behavior of search system to determine whether the design of on-chip system meets the design specification or not. However, model detection is constrained by the state space explosion problem, and the existing specification languages, such as computational tree logic and linear temporal logic, have limited description ability. In this paper, a method for detecting the symbol model of WISHBONE on-chip bus based on propositional projection temporal logic is proposed. In this method, the WISHBONE bus realized by Verilog hardware description language is transformed into the system model described by SMV, the modeling language of NuSMV model checking tool, and the expected properties of WISHBONE bus are described by propositional projective temporal logic. The PLSMC tool is used to verify whether the system model meets the desired properties. The experimental results show that this method can effectively verify the qualitative properties of the WISHBONE on-chip bus, as well as the quantitative properties such as time sensitivity and iteration.
【作者单位】：西安电子科技大学计算理论与技术研究所;
【基金】：国家“九七三”重点基础研究发展计划基金项目(2010CB328102) 国家自然科学基金项目(61003078,61272117,61133001,61272118,91218301,61322202,61202038)
【分类号】：TP336

【参考文献】