Sagar Chaki

Pritam Roy, Sagar Chaki, Pankaj Chauhan, Proceedings of the 22nd Design, Automation and Test in Europe Conference (DATE), March 25-29, 2019.

Abstract: 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.