在数字电路验证中使用模型检验

摘要：

形式化方法作为仿真方法的补充,为电路功能验证提供了新的途径.介绍了形式化验证方法之一,模型检验的理论基础和实现方法.介绍了分支时态逻辑CTL、CTL的固定点算法,二元决策图BDD,以及符号模型检验方法.最后使用SMV工具在一个CISC处理器的存储管理单元(MMU)上应用了模型检验,验证了模型检验在模块级验证中的可行性.

关键词：形式化验证、模型检验、分支时态逻辑、固定点、符号模型检验、二元决策图、SMV

所属期刊栏目：8

分类号：TP301.6(计算技术、计算机技术)

在线出版日期：2008-07-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：2038-2043