The project was started in Sept 2016 which was also the same month that I was first porting Fedora to RISC-V. Given the momentum behind RISC-V and also the huge amount of software now available it would obviously make sense to use a RISC-V compatible design. However hobbyists can do what they want, there's no reason to force someone who wants to design their own CPU to do it in any particular way.
The specification actually mentions RISC-V, and why I didn't use it. In hind sight, it's harder to decode the RISC-V instruction set than the one for the ZipCPU--to many holes in strange places.
Why are you being obtuse, rather than trying to be clear?
RISC-V is the major Free and Open CPU. RISC-V can run on FPGA. It's natural to want a comparison of this project against RISC-V, especially considering the write-up mentions the less successful OpenRISC project.
This page appears to have been written in summer of 2016. Back then RISC-V didn't even have a stable privileged instruction set yet, so there wasn't really a RISC-V to compare it to in a meaningful sense.
PicoRV32[0] targets some extremely low spec FPGAs. I have it running on ridiculously small and cheap FPGA[1] that has 8k LUTs and cost me £41 including tax and next day delivery.
However I repeat what I said above: hobbyists are free to design their own instruction sets, and good on them!
The ZipCPU and several peripherals can fit within an iCE40 8k using only about 5k LUTs--and that's with the multiply unit, the divide unit, the pipelined fetch unit, and a debugging bus infrastructure. While that isn't the full pipelined implementation neither do the caches fit, it is sufficient to be competitive with the picoRV.
The picorv32 is a nice little processor, but it's surprisingly inefficient in its use of FPGA resources compared to the performance it offers (which is very low.) For small FPGAs, it's far from being the best solution.
That said: there are a bunch of SOC construction tools for it, so that's definitely a redeeming factor.
But then again nearly every CPU runs on FPGA these days. 6502, Z80, various mainframe CPUs, x86, and more modern CPUs. Modern CPU development often goes via FPGA - after all, the CPU development tools are the same: Verilog, for example. Which you first synthesize to FPGA, and, after some testing rounds, to silicon.
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.
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.
> 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.
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.
> 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.
Does it really justify yet another RISC instruction-set?
Impressed that there's apparently already a GCC backend though.