Sufficiency-based filtering of invariants for Sequential Equivalence Checking

Inductive Invariants play critical roles in restricting the search space during Sequential Equivalence Checking (SEC), especially for those instances with few internal equivalent points. For large circuits, there can be too many potential invariants relating signals between the two circuits, thereby requiring much time to prove. However, we observe that a large portion of the potential invariants may not even contribute to equivalence checking. Moreover, equivalence checking can be significantly helped if there exists a method to check if a subset of potential invariants would be sufficient (e.g., whether two-nodes are enough or multi-nodes are also needed) prior to the verification step. In this paper, we address these problems and propose a sufficiency-based approach to identify useful invariants out of the initial potential invariants for SEC. Experimental results show that our approach can either demonstrate insufficiency of the invariants or select a small portion of them to successfully prove the equivalence property.