Formal Methodology Validates Cache-Coherence Protocol

摘要

Uncovering architectural problems early can prevent costly redesigns downstream. For example, it's not feasible to achieve sufficient coverage at the design level for cache-coherence protocol checking. That's because there's too much sequential depth. To verify a cache-coherence protocol, a tool must consider a range of traces that are both wide (in terms of starting and branching points) and deep (with long sequences of events).