Achieving high coverage in hardware equivalence checking via concolic verification

A concolic approach, called slec-cf, to find counterexamples (CEXs) to sequential equivalence between a high-level (e.g., SystemC) hardware description and an RTL (e.g., Verilog) is presented. slec-cf works by searching for CEXs over the possible values of a set of "control signals" in a depth-first lexicographic manner, and avoiding values that cannot be realized 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. Two strategies for concolic exploration are presented-searching all control signal values exhaustively, and only exploring values which share a common prefix with an initial random sample. In addition, two choices of control signals are proposed-the set of all MUX selectors in the RTL, and the MUX selectors that are derived from branch conditions in the SystemC description. Finally, slec-cf is made incremental by iteratively increasing the search depth, and set of control signals, and using a cache to reuse prior results. The approach is implemented on top an existing industrial sequential equivalence checker (slec) which compares C++/SystemC against RTL, created either manually, or by a high level synthesis tool, such as catapult. Experimental results indicate that slec-cf clearly outperforms random simulation in terms of finding CEXs quickly, and achieving coverage, over an industrial benchmark. On complex designs, incremental slec-cf demonstrates superior ability to achieve good coverage in almost all cases, compared to non-incremental slec-cf.