编号 zgly0000350800

文献类型 期刊论文

文献题名 基于增量可满足性的等价性检验方法

作者 李光辉  李晓维 

作者单位 浙江林学院信息工程学院  中国科学院计算技术研究所 

母体文献 计算机学报 

年卷期 2004,27(10)

页码 1388-1394

年份 2004 

分类号 TN431.2 

关键词 增量可满足性  等价性检验  组合电路  形式验证  数字集成电路  等价结点 

文摘内容 组合验证是数字集成电路形式化设计验证的重要方面.该文提出了一种基于增量布尔可满足性的组合等价性检验方法, 通过合理选择候选等价结点和增量可满足性算法来提高算法性能, 并通过对内部等价结点的置换及将等价关系转化为相应的合取范式公式, 避免了误判的发生, 又能缩小验证程序的搜索空间.针对ISCAS’85电路的实验结果表明, 该文提出的方法比以往同类方法更快、更强健?