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

Sequential Equivalence Check Using Cuts

在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.