MCMC Stimulus Generation for Constrained Random Simulation
Nathan Kitchen, Tobias Welp and Andreas Kuehlmann
As integrated circuits have grown in size and complexity, it has become increasingly difficult to verify their functions by directed testing. Many contemporary verification flows in industry have adopted a combination of constrained random testing and formal property checking. Despite considerable progress in formal methods in recent years, constrained random simulation remains the main workhorse of practical verification flows.
Due to the lack of research focus on constrained random verification, state-of-the-art tools still have serious limitations. Some tools generate random values efficiently at the expense of statistical quality. They sample random values from highly non-uniform distributions, resulting in skewed verification coverage. Other approaches generate values more uniformly but rely on methods (e.g., binary decision diagrams) that do not scale well to large designs.
In our research, we are addressing these shortcomings by building a solid theoretical foundation for constrained random verification and coverage maximization. Interestingly, there is a rich body of practical research on advanced sampling available from other domains such as Bayesian statistics and bio-informatics which have been mostly ignored by the verification community. In our work we first adapt these results to the needs of functional verification and extend the theoretical and practical work to handle large constraint sets mixing Boolean and integer constraints.
- N. Kitchen and A. Kuehlmann, "Stimulus Generation for Constrained Random Simulation," IEEE/ACM Int. Conference on Computer Aided Design (ICCAD), San Jose, CA, November 2007.
- N. Kitchen and A. Kuehlmann, "A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints," Computer-Aided Verification (LNCS 5643), Grenoble, France, July 2009.