Abstract: Generally, sequential equivalence circuit checking is to expand the sequential circuit into combinational circuit for verification. While in two sequential circuit to be verified, flip-flops is correspondent, identifying and matching corresponding flip-flops in the two sequential circuits to be verified is proved greatly effective. This paper builds a new miter circuit for Automatic Test Pattern Generation (ATPG) module, and then uses Boolean Satisfiability (SAT) tools to solve the Boolean function with timing frame unrolling transmission. Meanwhile, this method improves the SAT tool of information learning to accelerate the calculation process. Results on industrial- sized circuits ISCAS89 show these methods are both practical and efficient.