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

Placeholder

Departments

School / College / Institute

Program

KU Authors

Co-Authors

Yuan Yu
Brannon Batson

Publication Date

Language

Embargo Status

Journal Title

Journal ISSN

Volume Title

Alternative Title

Abstract

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.

Source

Publisher

Institute of Electrical and Electronics Engineers (IEEE)

Subject

Abstraction, Abstract data types, Computer systems, Computer software, Integrated circuit, Verification

Citation

Has Part

Source

Digest of Technical Papers - IEEE International Solid-State Circuits Conference

Book Series Title

Edition

DOI

item.page.datauri

Rights

Copyrights Note

Endorsement

Review

Supplemented By

Referenced By

0

Views

0

Downloads