Constraint Solver Development in Constrained Random Verification Methodology

Abstract:

Constrained random simulation is becoming the mainstream methodology in functional
verification. In order to achieve the verification closure, a high-throughput and
evenly-distributed constrained random pattern generator has become a must. In this
presentation, we propose a novel Range-Splitting heuristic and a Solution-Density
Estimation technique (RSSDE) to partition sample space. The chosen cutting planes
target to prune more infeasible subspaces so that the solution densities in other
subspaces increase correspondingly. In addition, with statistics-based analyses, the
estimated solution densities precisely predict the distribution of solutions. The
intermediate statistical information is recorded in a range-splitting tree (RS-tree). By
top-down random walking on the RS-tree, random pattern generation produces
evenly-distributed patterns with high throughput. Experimental results show that our
framework guarantees evenly-distributed stimuli and achieves more than 10X speedup
in average when compared to a state-of-the-art commercial generator.

The anticipated outline of my presentation is

1. Introduction to Constraint Solver in CRV
2. Previous Work
3. RSSDE Technique
4. Practical Issues
5. Experimental Results
¡@