基于切割法的时序电路等价验证  

Sequential Equivalence Check Using Cuts

作　　者：黄伟[1] 唐璞山[1] 

机构地区：[1]复旦大学专用集成电路与系统国家重点实验室,上海200433

出　　处：《复旦学报（自然科学版）》2006年第1期102-106,共5页Journal of Fudan University：Natural Science

基　　金：国家自然科学基金资助项目(90207002);国家"八六三"计划资助项目(2002AA1Z1460)

摘　　要：在Van Eijk时序电路等价验证算法中引入切割法,提出一种改进算法.由切割法引发的错反问题同时得到解决,合理的切割可以使时序电路等价验证只需较少时间.改进算法用SAT解答器作为计算引擎.实验结果表明,改进算法的运行速度约为原先算法的2倍.An improved algorithm which combines cut points technique with Van Eijk＇s sequential equivalence checking algorithm is presented. The false negative problem caused by the cut technique is solved, and reasonable cut results in less time for sequential equivalence checking. The calculating engine of the proposed algorithm is SAT-Solver. Experimental resuits show that the proposed algorithm can double the original speed.

关 键 词：半导体技术 计算机辅助设计 形式验证 SAT解答器 

分 类 号：TN402[电子电信—微电子学与固体电子学]