Fast Discovery of Illegal State Cubes for Sequential Equivalence Checking

Abstract

Sequential Equivalence checking has been and still is a challenging problem. Verifying two circuits that are structurally different but logically the same is very important and has many applications. Critical to the success of sequential equivalence checking is the determination of a sufficient portion of illegal states such that the two designs are equivalent outside of the illegal states. This work proposes a low-cost method to discover a subset of the illegal state space of a circuit by simulating and grouping some state variables to determine if any missing patterns are present. This thesis discusses the selection of simulated inputs, the grouping of flip-flops and what the missing patterns represent. Then all missing patterns are considered which are illegal state cubes and represent and compact them using BDDs. A BDD implementation was created to compact these illegal states more efficiently. Discussion is then done on the parameters of the BDD implementation design which can be used more efficiently given the situation. These illegal state cubes are considered to be implications which can be used to constrain a SAT solver. Results are then presented which show how effective these constraints are to proving equivalency using the SAT solver. Finally, the future work is discussed of discovering the illegal state space either faster or more completely.