Mining Unreachable Cross-Timeframe State-Pairs for Bounded Sequential Equivalence Checking

One common practice of checking equivalence for two sequential circuits often limits the timeframe expansion to a fixed number, and is known as bounded sequential equivalence checking (BSEC). Although the recent advances of Boolean satisfiability (SAT) solvers make combinational equivalence checking scalable for large designs, solving BSEC problems by SAT remains computationally inefficient. Therefore, this paper proposes a 3-stage method to exploit constraints to facilitate SAT solving for BSEC. The candidate set are first accumulated by checking each composition of functions derived by a data-mining algorithm for every two cross-timeframe flip-flop states. Each candidate can be further removed if it matches simulation data in history and its validity is finally confirmed through gate-level netlist. The verified set is feedbacked as constraints in SAT solving for the original BSEC problem. Experimental results show a 40X speedup in average on ISCAS 89 circuits.