Sequential equivalence checking based on k-th invariants and circuit SAT solving

In this paper, we first present the concept of the k-th invariant. In contrast to the traditional invariants that hold for all cycles, k-th invariants guarantee to hold only after the k-th cycle from the initial state. We then present a bounded model checker BMChecker and an invariant prover IProver, both of which are based on circuit SAT techniques. Jointly, BMChecker and IProver are used to compute the k-th invariants, and are further integrated with a sequential SAT solver for checking sequential equivalence. Experimental results demonstrate that the sequential equivalence checking framework can efficiently verify large industrial designs.