3 Years Ago- late 2020- I decided to start a RISC-V design in the Amaranth programming language. I wanted to make a CPU that was microcoded as practice. I got all the basic components connected together, but I got tired of working on the project and connecting components together before I started meaningfully writing the microcode (of course, by extension, this meant that the design didn't work at all).
Fast-forward to September 2023, Amaranth got a feature/RFC implemented that makes connecting HDL components easier. I decided to make an effort to finish what I started in 2020, and well...
Sentinel
It's not quite ready yet, but "perfect is the enemy of good/done". My RISC-V CPU works "good", it just needs some cleanup. Thus, I'm happy to announce Sentinel:
Sentinel is a microcoded RISC-V core, optimized for size before performance. It implements both the RV32I Base Integer Instruction Set and Zicsr Control and Status Register (CSR) Instructions Extension, for an ISA string of RV32I_Zicsr. Additionally, Sentinel implements the Machine Mode privileged spec and its corresponding CSRs, minus the memory-mapped Machine Timers (they aren't small :P).
One end goal of Sentinel was to be able to create a SoC with a Rust firmware that fits into 1280 LUTs/FFs. That way I can play with a SoC on the Lattice iCEStick. I managed to barely succeed with both a SoC (1270+ LUTs/FFs) and Rust firmware (1700 bytes out of 4kB used). The firmware demonstrates using a UART, a timer, GPIO, and interrupts using the former two as sources.
In addition to having a "known to work" toy firmware, the Sentinel CPU passes both RISC-V Formal and RISCOF test suites, in addition to my own tests. Future regressions of the RISC-V Formal and RISCOF test suites that I suspect I may trigger again will become part of my own bespoke tests as "witness traces" (basically, "here's the set of inputs that trigger a bug, save them and make a failing test that you can quickly analyze"). This way, I can improve my own test suite without needing to run RISC-V Formal (takes 20 minutes with 8 cores) and RISCOF (difficult to run outside of Linux) for every change I make. While I'm hesitant to say "Sentinel correctly implements the RISC-V spec for all possible pathological inputs", for now, I am fairly confident that the core will run any firmware you throw at it correctly in practice.1
Even though I spent a lot of time on preparing this when I could've been doing other things (like making sure I don't fall behind on upkeep, emails, reaching out to people, ya know, important stuff), I'm proud of the end result. Like it or not, I don't see RISC-V going away; I suspect knowledge of how to use RISC-V Formal, RISCOF, and how the Machine Mode privileged spec will come in handy in the future.
Microcode Musings
In the era of pipelines (in-order and out-of-order), microcoded designs seem to be a bit of a lost art. Today, microcode seems to relegated to CPU arch's complex instructions (x86 string insns, maybe "those newfangled ARM memcpy primitives? Idk...) that put a dent in the pure load-store philosophy. I didn't really know how to write a microcode before this project. Thankfully, I have some resources I can recommend:
-
[Bit-Slice Microprocessor Design by Mick And Brick] http://www.bitsavers.org/components/amd/bitslice/Mick_Bit-Slice_Microprocessor_Design_1980.pdf
This book is centered around the AMD Am2900 family of bit-slice chips. This family of chips is meant to be combined together to create a custom CPU, complete with a microcode. While the Am2900 chips might not be that relevant today, they were designed for microcode. So by extension of playing with Am2900 family chips and combining them together, you learn how to write a microcode.
-
The Wikipedia article is actually good now, or more likely, it was always fine and I just don't remember it at all. E.g. it gives examples and distinguishes horizontal vs vertical microcode.
-
One implementation of Zylin ZPU is microcoded, and I found that useful to study.
Footnotes
- After adding a few more tests, I will be able to at least say "Sentinel is correct with respect to the RISC-V Formal spec after reset". Note that RISC-V Formal is tested against the Spike RISC-V C++ model, which is in turn tested against the SAIL RISC-V OCaml/"gold standard" model. So RISC-V Formal's spec is probably okay.
An "after reset" Bounded Model Check (BMC) is a weaker guarantee than "correct for all time under all conditions". However RISC-V Formal offers a prove option (k-induction) for "correct for all time under all conditions" that I consider enabling in the future. Note that it's sometimes impossible to prove something holds for all time under all conditions without restrictions. See RISC-V Formal's liveness ("do we make progress?") discussion:
It might be neccessary to add some bounded fairness constraints to the design for this check to succeed.
This discussion also applies to prove; Galaxy Brain Meme Without extra constraints, you can (usually) make a proof-for-all-time-and-conditions fail by cleverly stopping forward progress to create a counterexample :).