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

Verification of PIC Based on Symbolic Model Checking

作　　者：刘建元[1] 

机构地区：[1]西安邮电学院,西安710061

出　　处：《微电子学与计算机》2002年第5期62-64,共3页Microelectronics & Computer

基　　金：国家自然科学基金资助项目(69473017)

摘　　要：随着程序或电路规模的增大,状态数目将呈指数增加而引起组合爆炸。符号模型检验是形式化方法的一个重要方面,可以处理大规模的数据结构和控制序列,缓和了组合爆炸问题。文章介绍了符号模型检验的原理和方法,利用验证工具VIS验证了8位微处理器PIC的一些关键属性,并给出实验结果。Exponentially increasing of the state number of a system causes the combination exploring with the scale of program or circuit increasing. Symbolic module checking which deals with large-scale data structure and the sequenceof control treats with the combination exploring. This paper mainly introduces the principle and methods of symbolic module checking. Some of the important features of a microprocessor PIC are verified using VIS.

关 键 词：符号模型检验 硬件验证 微处理器 有限状态机 分支时态逻辑 有序二叉判定图 

分 类 号：TP332[自动化与计算机技术—计算机系统结构]