结合通用割集和专用割集的组合电路验证方法  

Combinational equivalence checking method based on universal cut and special cut

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

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

出　　处：《浙江大学学报（工学版）》2006年第9期1511-1515,共5页Journal of Zhejiang University：Engineering Science

基　　金：国家自然科学基金资助项目(90207002)

摘　　要：为了提高组合电路的等价性验证速度,提出了一种利用电路内部等价信息的新型验证方法.该方法结合了通用割集和专用割集.从原始输出进行回溯得到通用割集,用通用割集验证所有候选等价点(CEP)的等价性.从特定候选等价点进行回溯得到专用割集,通过消除高层次结点间的依赖关系对专用割集进行优化,用专用割集验证特定候选等价点的等价性.实验结果表明,与传统依赖性处理策略相比,该验证方法中的依赖性处理策略减少了验证时间.与只基于通用割集或专用割集的验证方法相比,该方法可以使组合电路的验证速度明显提高.To increase the speed of equivalence checking for combinational circuits, a new method using internal equivalence information of circuits in verification was proposed. Universal cut and special cut were combined in the method. Universal cut was generated by tracing from primary outputs, and equivalence of all candidate equivalent points （CEPs） was verified by using universal cut. After special cut was generated by tracing from a special pair of CEP, dependencies among high level nodes in special cut were removed for optimization, and the equivalence for the special pair of CEP was verified by using special cut. Experimental results show that compared with traditional dependency removal strategy, the dependency removal strategy in the method can reduce the time of verification. Compared with the method only using universal cut or special cut, the method can obviously improve the speed of verification for combinational circuits.

关 键 词：形式验证 通用割集 专用割集 依赖性 

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