Architecting hierarchical coherence protocols for push-button parametric verification
Recent work in formal verification theory and verification-aware design has sought to bridge the divide between the class of protocols architects want to design and the class of protocols that are verifiable with state of the art tools. Particularly, the recent Neo work in formal verification theory, for the first time, formalizes how to compose flat subprotocols with an arbitrary number of nodes into a hierarchy while maintaining correct behavior. However, it is unclear if this theory scales to realistic systems. Moreover, there is a diversity of systems architects would be interested in, to which it is not clear if the theory applies. In this paper, we show how the abstract Neo theory can be leveraged to design a realistic hierarchical coherence protocol. As such, we present the first realistic hierarchical coherence protocol verified with fully-automated (push-button) verification tools for all scales and tree configurations. We explore the practical limitations posed by both the theory and the verification tools in designing this verifiable hierarchical protocol. We experimentally evaluate our protocol, comparing it to more complex protocols that have optimizations prohibited by the theory and verification tool. Finally, we discuss how a variety of system configurations and protocols architects might be interested in can be adapted to the Neo theory, which we hope opens up the theory to future work in verificationaware protocol design.
