High Coverage Concolic Equivalence Checking

摘要

A concolic approach, called Slec-Cf, to check sequential equivalence between a high-level (e.g., C++/SystemC) hardware description and an RTL (e.g., Verilog) is presented. Slec-Cf searches for counterexamples over the possible values of a set of "control signals" in a depth-first lexicographic manner, avoiding values that are unrealizable by any concrete input. In addition, Slec-Cf respects user-specified design constraints during search, thus only producing stimuli that are of relevance to users. It is a superior alternative to random simulations, which produce an overwhelming number of irrelevant stimuli for user-constrained designs, and are therefore of limited effectiveness. To handle complex designs, we present an incremental version of Slec-Cf, which iteratively increases the search depth, and set of control signals, and uses a cache to reuse prior results. We implemented Slec-Cf on top an existing industrial tool for sequential equivalence checking. Experimental results indicate that Slec-Cf clearly outperforms random simulation in terms of coverage achieved. On complex designs, incremental Slec-Cf demonstrates superior ability to achieve good coverage in almost all cases, compared to non-incremental Slec-Cf.