| 基于符号模型检验的硬件验证 |
| |
| 引用本文： | 刘建元. 基于符号模型检验的硬件验证[J]. 微电子学与计算机, 2002, 19(5): 62-64 |
| |
| 作者姓名： | 刘建元 |
| |
| 作者单位： | 西安邮电学院,西安,710061 |
| |
| 基金项目： | 国家自然科学基金资助项目(69473017) |
| |
| 摘 要： | 随着程序或电路规模的增大，状态数目将呈指数增加而引起组合爆炸。符号模型检验是形式化方法的一个重要方面，可以处理大规模的数据和控制序列，缓和了组合爆炸的问题。文章介绍了符号模型检验的原理和方法，利用验证工具VIS验证了8位微处理器PIC的一些关键属性，并给出实验结果。
|
| 关 键 词： | 符号模型检验 硬件验证 微处理器 有限状态机 分支时态逻辑 有序二叉判定图 |
| 修稿时间： | 2001-11-29 |
Verification of PIC Based on Symbolic Model Checking |
| |
| LIU Jian yuan. Verification of PIC Based on Symbolic Model Checking[J]. Microelectronics & Computer, 2002, 19(5): 62-64 |
| |
| Authors: | LIU Jian yuan |
| |
| Abstract: | 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. |
| |
| Keywords: | Finite-state machine Computational tree logic Ordered binary decision diagram Symbolic model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
