An algorithmic approach to design exploration

In recent years, the technique of symbolic model checking has proven itself to be extremely useful in the verification of hardware. However, after almost a decade, the use of model checking techniques is still considered complicated, and is mostly practiced by experts. In this paper we address the question of how model checking techniques can be made more accessible to the hardware designer community. We introduce the concept of exploration through model checking, and demonstrate how, when differently tuned, the known techniques can be used to easily obtain interesting traces out of the model, rather than used for the discovery of hard-to-find bugs. We present a set of algorithms, which support the exploration flavor of model checking. © Springer-Verlag Berlin Heidelberg 2002.