用VIS验证微处理器PIC  

Verification of the Microprocessor PIC

作　　者：杜慧敏[1] 刘建元[1] 韩俊刚[1] 高德远 

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

出　　处：《计算机辅助设计与图形学学报》2000年第5期390-395,共6页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金!( 69473 0 17)

摘　　要：近年来 ,二叉判定图 BDD(Binary Decision Diagram )和符号模型检验在形式化验证数字电路设计中取得了突破性进展 .文中介绍了符号模型检验的基本原理和方法 ,重点介绍如何用 VIS系统验证微处理器 PIC设计的正确性 .利用 VIS证明了 PIC设计部分电路的等价性 ,发现了一个设计错误并证明了 PIC中一些重要模块的特性 .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.

关 键 词：微处理器 检验 VIS 二叉决策图 PIC 

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