Publications without Fulltext

Permanent URI for this collectionhttps://hdl.handle.net/20.500.14288/3

Browse

Filter results by typing the first few letters
Now showing 1 - 1 of 1
  • Placeholder
    PublicationMetadata only
    Using a formal specification and model checker to monitor and direct simulation
    (Institute of Electrical and Electronics Engineers (IEEE), 2003) Yuan Yu; Brannon Batson; Department of Computer Engineering; Taşıran, Serdar; Faculty Member; Department of Computer Engineering; College of Engineering; N/A
    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 identities 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.