| 用VIS验证微处理器PIC |
| |
| 引用本文： | 杜慧敏,刘建元,韩俊刚,高德远.用VIS验证微处理器PIC[J].计算机辅助设计与图形学学报,2000,12(5):390-395. |
| |
| 作者姓名： | 杜慧敏 刘建元 韩俊刚 高德远 |
| |
| 作者单位： | 西安邮电学院ASIC中心,西安,710061 |
| |
| 基金项目： | 国家自然科学基金!( 69473 0 17) |
| |
| 摘 要： | 近年来，二叉判定图ＢＤＤ和符号模型检验在形式验证数字电路设计中取得了突破性进展，文中介绍了符号模型检验的基本原理和方法，重点介绍了如何用ＶＩＳ系统验证微处理器ＰＩＣ设计的正确性。利用ＶＩＳ证明了ＰＩＣ设计部分电路的等价性。发现了一个设计错误并证明了ＰＩＣ中一些重要模块的特性。
|
| 关 键 词： | 微处理器 检验 VIS 二叉决策图 PIC |
Verification of the Microprocessor PIC |
| |
| DU Hui-Min,LIU Jian-Yuan,HAN Jun-Gang,GAO De-Yuan.Verification of the Microprocessor PIC[J].Journal of Computer-Aided Design & Computer Graphics,2000,12(5):390-395. |
| |
| Authors: | DU Hui-Min LIU Jian-Yuan HAN Jun-Gang GAO De-Yuan |
| |
| Abstract: | Binary Decision Diagram and symbolic model checking has made breakthrough in digital circuit design. This paper introduces the principle and methods of model checking and focuses on how to validate the correctness of a microprocessor PIC by VIS Equivalence of part design of PIC is proved, an important feature of PIC is verified and a bug is found. |
| |
| Keywords: | Binary Decision Diagram computational tree logic equivalence check symbolic model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
