Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor
- Yuan Yu
Proceedings of the 3rd IEEE International Workshop on Microprocessor Test and Verification (MTV '02) |
Published by Institute of Electrical and Electronics Engineers, Inc.
We describe a technique for verifying that a hardware design correctly implements a protocol. The application of this technique to verifying the cache and memory controllers of the Alpha 21364 EV7 microprocessor against a formal speci cation of the EV7 cache coherence protocol is presented.
© 2002 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.