4 ms·

> we verify a fairly realistic implementation of a multicore shared-memory system with two types of components: memory system and processor. Both components inc

by snaky 8y ago

> we verify a fairly realistic implementation of a multicore shared-memory system with two types of components: memory system and processor. Both components include nontrivial optimizations, with the memory system employing an arbitrary hierarchy of cache nodes that communicate with each other concurrently, and with the processor doing speculative execution of many concurrent read operations. Nonetheless, we prove that the combined system implements sequential consistency. To our knowledge, our memory-system proof is the first machine verification of a cache-coherence protocol parameterized over an arbitrary cache hierarchy, and our full-system proof is the first machine verification of sequential consistency for a multicore hardware design that includes caches and speculative processors. https://deepspec.org/entry/Paper/Modular.20Deductive.20Verification.20of.20Multiprocessor.20Hardware.20Designs https://deepspec.org/entry/Paper/Modular.20Deductive.20Verif...

aseipp 8y ago
That paper doesn't have anything to do with what the original poster said, which is that extremely large scale VLSI-style designs don't use FPGAs, but instead use large-scale, extremely expensive and fast simulators instead. That's basically correct, regardless of the kinds of formal methods that are in play: simulation is vastly cheaper and more feasible at large scales, so much so that people instead buy hardware accelerators for simulation to improve development time and get reasonable turnaround on complex components. Smaller-scale embedded systems or bespoke designs can get away with full FPGA flows in order to do low-scale deployment/development (e.g. SiFive's CPU cores all run this way, and you can run them) -- and pretty much all hobbyist CPUs do so. But to say all modern CPUs use FPGAs in their development cycle is overstating it a bit. There's simply no devices that exist the kind of logic density needed to realistically model many large scale, high-volume designs you see today, not to mention the unbelievable synthesis times you'd have to endure.
- snaky 8y ago
  > 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...
  - zipcpu 8y ago
    All of the ZipCPU's cache implementations have been formally verified using SymbiYosys--an open source, free-as-beer product.

by snaky 8y ago

aseipp 8y ago

That paper doesn't have anything to do with what the original poster said, which is that extremely large scale VLSI-style designs don't use FPGAs, but instead use large-scale, extremely expensive and fast simulators instead. That's basically correct, regardless of the kinds of formal methods that are in play: simulation is vastly cheaper and more feasible at large scales, so much so that people instead buy hardware accelerators for simulation to improve development time and get reasonable turnaround on complex components. Smaller-scale embedded systems or bespoke designs can get away with full FPGA flows in order to do low-scale deployment/development (e.g. SiFive's CPU cores all run this way, and you can run them) -- and pretty much all hobbyist CPUs do so. But to say all modern CPUs use FPGAs in their development cycle is overstating it a bit. There's simply no devices that exist the kind of logic density needed to realistically model many large scale, high-volume designs you see today, not to mention the unbelievable synthesis times you'd have to endure.

snaky 8y ago
> 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...
- zipcpu 8y ago
  All of the ZipCPU's cache implementations have been formally verified using SymbiYosys--an open source, free-as-beer product.