Using a formal specification and a model checker to monitor and direct simulation
- Resource Type
- Conference
- Authors
- Tasiran, S.; Yuan Yu; Batson, B.
- Source
- Proceedings 2003. Design Automation Conference (IEEE Cat. No.03CH37451) Design automation conference Design Automation Conference, 2003. Proceedings. :356-361 2003
- Subject
- Computing and Processing
Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Formal specifications
Monitoring
Protocols
Hardware
Design methodology
Permission
Formal verification
State-space methods
Microprocessors
Coherence
- Language
We describe a technique for verifying that a hardware design correctly implements a protocol-level format specification. Simulation steps are translated to protocol state transitions using a refinement map and then verified against the specification using a model checker. On the specification state space, the model checker collects coverage information and identifies states violating certain properties. It then generates 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.