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.