Combinational techniques for sequential equivalence checking

Often sequential logic synthesis can lead to substantially easier verification problems, compared to the general-case for sequential equivalence checking (SEC). We prove some general theorems about when SEC can be reduced to combinational equivalence checking (CEC). These can be applied to many sequential clock gating transforms, where correctness is argued intuitively using a finite unrolling of a sequential design. A method based on these theorems was applied to six large industrial examples. It completed on all examples and was about 30x faster on the three examples where the conventional engine was able to finish.