摘要
近年来 ,二叉判定图 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.
出处
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2000年第5期390-395,共6页
Journal of Computer-Aided Design & Computer Graphics
基金
国家自然科学基金!( 69473 0 17)
关键词
微处理器
检验
VIS
二叉决策图
PIC
Binary Decision Diagram, computational tree logic, equivalence check, symbolic model checking
