| 结合无依赖性割集和量化的等价性验证 |
| |
| 引用本文： | 卢永江,严晓浪,葛海通,杨军. 结合无依赖性割集和量化的等价性验证[J]. 计算机辅助设计与图形学学报, 2005, 17(10): 2215-2219 |
| |
| 作者姓名： | 卢永江 严晓浪 葛海通 杨军 |
| |
| 作者单位： | 浙江大学超大规模集成电路设计研究所,杭州,310027;浙江财经学院信息学院,杭州,310012;浙江大学超大规模集成电路设计研究所,杭州,310027 |
| |
| 基金项目： | 国家自然科学基金（90207002） |
| |
| 摘 要： | 提出一新的验证算法，利用电路拓扑信息选择有效割集，以减小验证规模，并对割集进行无依赖性处理，减少伪错误发生概率，提高验证效率；同时，利用启发式信息选择复杂度较高的节点变量进行量化，进一步减小二叉决策图（BDD）的内存要求．最后用ISCAS’85电路的实验结果证明了该算法的有效性．
|
| 关 键 词： | 二叉决策图 形式验证 割集 量化 |
| 收稿时间： | 2004-06-16 |
| 修稿时间： | 2004-06-162004-09-20 |
Combining Independent Cuts and Quantification for Equivalence Checking |
| |
| Lu Yongjiang,Yan Xiaolang,Ge Haitong,Yang Jun. Combining Independent Cuts and Quantification for Equivalence Checking[J]. Journal of Computer-Aided Design & Computer Graphics, 2005, 17(10): 2215-2219 |
| |
| Authors: | Lu Yongjiang Yan Xiaolang Ge Haitong Yang Jun |
| |
| Affiliation: | 1 Institute of VLSI Design, Zhejiang University, Hangzhou 310027; 2 Information School, Zhejiang University of Finance and Economics, Hangzhou 310012 |
| |
| Abstract: | 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. |
| |
| Keywords: | BDD formal verification cut quantification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
