用VIS验证微处理器PIC

摘要：

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

关键词：二叉决策图、分支时态逻辑、等价性检验、符号模型检验

所属期刊栏目：12

分类号：TP301.1(计算技术、计算机技术)

资助基金：中国科学院资助项目69473017

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：390-395