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