About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Paper
An algorithmic approach to design exploration
Abstract
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.