An Integrated Methodology for the Verification of Directory-Based Cache Protocols

The complexity of directory based protocols has motivated us to build a hardware emulator or testbed for the rapid prototyping of various protocols under various memory consistency models for CC-NUMA architectures. To implement and verify new protocols rapidly on the testbed, we have developed an overall methodology around a set of tools applicable to different aspects of the verification of a protocol, i.e., protocol-intrinsic errors, memory access ordering errors and protocol implementation errors. These tools include formal verification techniques, architecture simulators and hardware mechanisms implemented in the FPGAs of the testbed.