CSP-Based RTL-Datapath Satisfiability Solving: Strategies and Comparisons

This paper studies how constraint satisfaction problem (CSP) algorithms, as well as various CSP strategies behave in VLSI RTL-datapath satisfiability solving. For this, we first present the method of using a CSP engine to solve the RTL-datapath satisfiability problem. Next we demonstrate the respective virtue of the five basic CSP strategies BT, BJ, CBJ, BM, and FC by examples. Then the five basic strategies, along with other four hybrid strategies BMJ, BM-CBJ, FC-BJ and FC-CBJ are tested on two large RTL circuits. We compare the strategies in much detail both in the number of checking operations and runtime. The main contribution of our work is demonstrating the applicability of CSP techniques to the VLSI verification domain, and that careful selection of the strategies is important.