A Modified Frame Expansion Based Sequential Equivalence Checking Algorithm

A new frame-expansion based sequential equivalence checking algorithm is proposed.It derives from the induction-based model checking algorithm,and merges the checking processes of base condition and induction condition using our simplified unsatisfiable core extraction in SAT problem.Furthermore,in order to reduce the state space searched during frame expansion,structural fixed-point technique is exploited,and quasi dynamic unique state constraint is proposed.Experimental results show that during the expansion of circuit frames,the elapsed time of our method increases much slower than that of the induction based algorithm.The total elapsed time is also promising when verifying sequentially optimized circuits.