Sequential equivalence checking using cuts

This paper presents an algorithm which is an improvement of Van Eijk´s algorithm (2000) by incorporating a cutpoints technique (Kuelhmann and Krohm, 1997). Combinational verification often uses the technique to convert large scale circuits to several small ones, which will be verified separately. Reasonable cuts can bring less time consuming to combinational verification. We embed the technique into sequential equivalence checking. Experimental results show that the proposed method can achieve about 2× speedup over the original one.