结合无依赖性割集和量化的等价性验证  

Combining Independent Cuts and Quantification for Equivalence Checking

作　　者：卢永江[1] 严晓浪[1] 葛海通[1] 杨军[1] 

机构地区：[1]浙江大学超大规模集成电路设计研究所

出　　处：《计算机辅助设计与图形学学报》2005年第10期2215-2219,共5页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金(90207002)

摘　　要：提出一新的验证算法,利用电路拓扑信息选择有效割集,以减小验证规模,并对割集进行无依赖性处理,减少伪错误发生概率,提高验证效率;同时,利用启发式信息选择复杂度较高的节点变量进行量化,进一步减小二叉决策图(BDD)的内存要求.最后用ISCAS’85电路的实验结果证明了该算法的有效性.In this paper, a novel algorithm is presented to enhance the effectiveness of the binary decision diagram（BDD） engine. It is proposed to select effective cut with no dependence remaining by using the circuit topology structure. And at the same time according to the heuristic information, we select more complex variables for quantification. Experimental results applied to ISCAS85 benchmark circuits demonstrate the practicability of our approach.

关 键 词：二叉决策图 形式验证 割集 量化 

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