Cache-coherent protocols and the RTL implementations of the components of the protocols provide unique verification challenges. In this article Rajeev Ranjan consider the Jasper formal solution that they have built in collaboration with ARM.
Initially, we must model and verify the protocol to demonstrate that it adheres to high-level, cache-coherence rules. He identified 6 challenges which he discusses in the article
- Creating a machine-readable specification,
- Ensuring protocol model soundness,
- Debugging the protocol model,
- Verifying the protocol model,
- Using the model for protocol comprehension, and
- Creating a reusable protocol model for RTL verification.