2011 IEEE International High Level Design Validation and Test Workshop (2011)
Napa Valley, CA, USA
Nov. 9, 2011 to Nov. 11, 2011
Wei Hu , Department of Electrical and Computer Engineering, Virginia Tech, Blacksburg, Virginia, USA
Huy Nguyen , Department of Electrical and Computer Engineering, Virginia Tech, Blacksburg, Virginia, USA
Michael S. Hsiao , Department of Electrical and Computer Engineering, Virginia Tech, Blacksburg, Virginia, USA
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.
M. S. Hsiao, W. Hu and H. Nguyen, "Sufficiency-based filtering of invariants for Sequential Equivalence Checking," 2011 IEEE International High Level Design Validation and Test Workshop(HLDVT), Napa Valley, CA, USA, 2011, pp. 1-8.