Abstract
This paper presents a novel simplification method based on the range-equivalent circuit optimization technique for the SAT-based bounded sequential equivalence checking (BSEC), which verifies the functional equivalence of two sequential circuits with a bounded depth by using a SAT solver. The key idea is to optimize the circuits in BSEC model while keeping the output to the next state range-equivalent. Instead of unrolling the two sequential circuits, we first minimize them with range-equivalent circuit technique. This is because the previous timeframes can be seen as a pattern generator that feeds input patterns to the next timeframe and only the range, i.e., all the output combinations, are required information for the next timeframes. Using the known condition that two sequential circuits are functionally equivalent within k - 1 timeframes, we enhance their equivalence checking with the bounded depth k. Given two sequential circuits to be verified, we first verify the functional equivalence of their 1st timeframes. If their 1st timeframes are non-equivalent, these two circuit are non-equivalent. Conversely, if their 1st timeframes are equivalent, we simplify the circuit consisting of their 1st timeframes by using the conventional logic optimization methods followed by the range-equivalent circuit technique. Next, we use this simplified circuit to drive the next timeframes of these two circuits, and then verify their functional equivalence again. This process repeats until the timeframes under verification are non-equivalent or a user-specified bounded depth has been reached. The experimental results show that the proposed simplification method can save more verification time and provide more accurate verification compared to the previous enhancement method on the set of IWLS 2005 benchmarks.