基于符号模型检验的硬件验证

• 作者: 刘建元
• 来源期刊: 微电子学与计算机
• 关键词: 有限状态机 分支时态逻辑 有序二叉判定图 符号模型检验
• 年，卷（期）: 2002,（5）
• 所属期刊栏目: 应用与开发
• 页码范围: 62-64
• 页数: 3页
• 分类号: TP3
• 语种: 中文
• DOI: 10.3969/j.issn.1000-7180.2002.05.022

摘要

随着程序或电路规模的增大,状态数目将呈指数增加而引起组合爆炸.符号模型检验是形式化方法的一个重要方面,可以处理大规模的数据结构和控制序列,缓和了组合爆炸问题.文章介绍了符号模型检验的原理和方法,利用验证工具VIS验证了8位微处理器PIC的一些关键属性,并给出实验结果.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘建元		8	27	3.0	5.0