To model check or not to model check

In the past, hardware design validation has relied primarily on simulation. New techniques such as model checking have been introduced but no objective study investigating the advantages such techniques provide over simulation has been made. Simulation is model checking over a trace elicited by executing a test vector; model checking can be viewed as exhaustive simulation. Each has its own set of advantages and limitations. A platform, “Sherlock”, was available wherein one could use properties or specifications expressed as CTL-like formulae interchangeably for checking simulation runs or for model checking. In this paper we describe and present results from an experimental study undertaken on a real implementation to better understand the efficacies of the two methods. We also present improved methods for accommodating liveness, fairness (of arbitration) and existence conditions in simulation and outline some techniques for writing implementation-independent properties for model checking