Abstract
This paper presents a method based on range-equivalent circuit technique for SAT-based bounded sequential equivalence checking. Given two sequential circuits to be verified, instead of straightforward unrolling the miter of two sequential circuits, we iteratively minimize the miter with a range-equivalent circuit technique before adding a new timeframe. This is because the previous timeframes can be seen as a pattern generator that feeds input patterns to the next timeframe and only the ranges of previous timeframes are required information for the next timeframe. Experimental results show that the proposed method saved up to 91 percent of verification time for reaching the same bounded depth compared with previous work on a set of IWLS2005 benchmarks.