> The scope of verifiable components is fundamentally limited by the state-space-explosion problem. For example, in order to verify cache-coherence protocols wi

> The scope of verifiable components is fundamentally limited by the state-space-explosion problem. For example, in order to verify cache-coherence protocols with Murphi [Dill et al.1992], a widely used model checker designed for that exact task, at one point the biggest system that could be verified had only 3 cores interacting with a single-address memory having two potential values. While improvements to algorithms and hardware (for running the analysis) continually increase the feasible system size, there are fundamental limitations of such tools that explore finite state spaces, in the face of exponential growth in state spaces as we add processor cores or memory addresses. > In this paper, we introduce the Kami framework for the Coq proof assistant, which brings this style of development and verification to the world of computer architecture, simultaneously reversing all of the weaknesses enumerated above for most hardware-verification tools. Kami makes it possible to code and verify a fairly realistic processor within Coq and then extract it to run on FPGAs (and almost certainly in silicon, though we have not yet had the opportunity to fabricate a “real” chip). We also emphasize that our use of “verified” is more in the tradition of CompCert [Leroy 2006] or seL4 [Klein et al. 2009] than of the day-to-day practices of verification engineers in the hardware industry: we prove that a system with any number of shared-memory cores with associated coherent caches correctly implements the functional-correctness specification of our instruction set, with respect to sequential consistency. https://deepspec.org/entry/Paper/Kami.3A+A+Platform+for+High.2DLevel+Parametric+Hardware+Specification+and+its+Modular+Verification https://deepspec.org/entry/Paper/Kami.3A+A+Platform+for+High...