3 ms·

You may be able to run certain modern CPU units on an FPGA, maybe even one modern core, but compare the 4 million LUTs the biggest FPGA has to the 19 billion tr

You may be able to run certain modern CPU units on an FPGA, maybe even one modern core, but compare the 4 million LUTs the biggest FPGA has to the 19 billion transitors a 32 core AMD EPYC has. With a LUT wildly variable equivalence of 1 to 1-50 ASIC transistors depending on the logic implemented, there's still one order of magnitude gap between them at best. In practice, Verilog simulators are used instead, they're slow as a dead horse on smack, but it's the only way to have full (logic) system integration of such big designs.

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.
monocasa 8y ago
There's a halfway point, confusingly called emulators. You get a whole rack of FPGAs (or sometimes giant arrays of tiny little CPUs that only run boolean ops) connected to eachother, running at 10s of Mhz with the signals between them multiplexed.
slededit 8y ago
Most of a modern processor is cache. You could likely fit the actual core on a relatively large FPGA. The cache would be harder.

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.

monocasa 8y ago

There's a halfway point, confusingly called emulators. You get a whole rack of FPGAs (or sometimes giant arrays of tiny little CPUs that only run boolean ops) connected to eachother, running at 10s of Mhz with the signals between them multiplexed.

slededit 8y ago

Most of a modern processor is cache. You could likely fit the actual core on a relatively large FPGA. The cache would be harder.