Sequential equivalence checking based on K-th invariants and circuit

In this paper, we first present the concept of the k-th invari-ant. 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 in-variants, and are further integrated with a sequential SAT solver for checking sequential equivalence. Experimen-tal results demonstrate that the new sequential equivalence checking framework can efficiently verify large industrial designs. I