Sciweavers

DAC
2003
ACM

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

14 years 4 months ago
Using a formal specification and a model checker to monitor and direct 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 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. Categories and Subject Descriptors
Serdar Tasiran, Yuan Yu, Brannon Batson
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2003
Where DAC
Authors Serdar Tasiran, Yuan Yu, Brannon Batson
Comments (0)