Abstract

Constrained random simulation is the main workhorse in today’s hardware verification flows. It requires the random generation of input stimuli that obey a set of declaratively specified input constraints, which are then applied to validate given design properties by simulation. The efficiency of the overall flow depends critically on (1) the performance of the constraint solver and (2) the distribution of the generated solutions. In this paper we discuss the overall problem of efficient constraint solving for stimulus generation for mixed Boolean/integer variable domains and propose a new hybrid solver based on Markov-chain Monte Carlo methods with good performance and distribution. 1

Nathan KitchenAndreas Kuehlmann

Topics

Simulation Techniques and ApplicationsFormal Methods in VerificationEmbedded Systems Design TechniquesComputer scienceSolver