A robust constraint solving framework for multiple constraint sets in Constrained Random Verification

To verify system-wide properties on SoC designs in Constrained Random Verification (CRV), the default set of constraints to generate patterns could be overridden frequently through the complex testbench. It usually results in the degradation of pattern generation speed because of low hit-rate problems. In this paper, we propose a technique to preprocess the solution space under each constraint set. Regarding the similarity between constraint sets, the infeasible subspaces under a constraint set help identify the infeasible subspaces under another constraint set. The profiled results under each constraint set are then stored in a distinct range-splitting tree (RS-Tree). These trees accelerate pattern generation under multiple constraint sets and, simultaneously, ensure the produced patterns are evenly-distributed. In our experiments, our framework achieved 10X faster pattern generation speed than a state-of-art tool in average.