Using a formal specification and a model checker to monitor and guide simulation

We describe a technique for verifying that a hardware design correctly implements a protocol-level formal specification. Simulation steps are translated to protocol state transitions using a refinement map and then verified against the spec-ification using a model checker. On the specification state space, the model checker collects coverage information and identifies states violating certain properties. It then gener-ates protocol-level traces to these coverage gaps and error states. This technique was applied to the multiprocessing hardware of the Alpha 21364 microprocessor and the cache coherence protocol. We were able to generate an error trace which exercised a bug in the implementation that had not been discovered before a prototype was built