Several of you have asked me, following the ZipCPU ISA introduction article, to present instructions for building and trying out the ZipCPU for yourselves. I would like to do that. Indeed, I’m planning on it. If the Lord is willing, this will be my next article. If I get stuck along the way and it takes too long to get there, then I might just pause and describe a quadratic interpolator first, but if the Lord remains willing we’ll still get there.

This week, however, I’ve gotten stuck into the “just-one-more” (fill in the blank) change loop. Most of these changes have centered around formal verifying that the various components of the ZipCPU works as designed.

At first the task was easy–I just started building formal verification proofs for the little components within the ZipCPU–you know, the peripherals that just count instructions, or the one that justs counts down to zero and then creates an interrupt. In each case, I’ve gotten to the point where I think I’m ready to post the “here’s how to get started article”, and I think to myself, “Just one more proof.” I mean, how hard can a simple timer be, for example?

Well, that simple timer was harder to formally verify than I expected.

Then, after I wrote up the chart below, things started to become a challenge. Surely I could formally verify the DMA controller, right? I wouldn’t want to present the ZipCPU to others if there was a subtle bug within the DMA controller that formal methods could find, right? The DMA controller, I told myself, should be easy: I’ve already put together the set of formal Wishbone properties necessary to make certain it works, the hard work has been done, right?

One day later, I have a wonderful proof that my DMA controller works, but I’m no closer to writing the getting started article. Of course, it didn’t help that I adjusted how I expressed the wishbone properties, and so other components–notably the (yet to be integrated) MMU had to be adjusted to work with this new property description as well …

However, with everyone of these projects, I’m getting closer and closer to being able to formally verify the entire CPU. Even further, I intended to do a full proof, including not only bounded model checking but induction as well.

Just so you see how far I’ve gotten, here’s a list of the RTL components in the ZipCPU project, together with whether or not I’ve managed to finish formally verifying the component or not.

Project Component Purpose Status
ZipCPU      
  prefetch Single Insn Prefetch Proven
  dblfetch Two Insn Pipelined Prefetch Proven
  pfcache Prefetch and integrated instruction cache Proven
  idecode Instruction decoder Proven
  div Divide module Proven
  memops Memory Interface Module Proven
  pipemem Memory Module, supporting pipelined mem access Proven
  icontrol Interrupt controller Proven
  zipjiffies I/O Scheduling peripheral Proven
  zipcounter Performance counter Proven
  ziptimer Count-down timer Proven
  wbdmac CPU DMA Controller Proven
  zipmmu External MMU peripheral Proven
  busdelay A timing saving bus delay Proven
  wbpriarbiter A wishbone priority arbiter Proven
  wbdblpriarb A priority arbiter for a pair of shared wishbone interfaces Proven
  cpuops ALU component (Not started)
  zipcpu Master CPU controller (Not started)
  zipbones CPU Container (Not started)
  zipsystem CPU Container with Peripherals (Not started)
Fig 1. Components of a ZipSystem

Pictorially, you can see most of these components in the diagram of the ZipSystem shown to the right in Fig 1. I’ve proven all of the peripheral components shown in boxes on the right, as well as all of the sub-components within the CPU in the yellow box on the left. (The CPU still doesn’t have an FPU component, and the ALU was forgotten when I initially built the table above.) The large yellow box on the left that is the CPU within the ZipSystem still remains to be proven, as does the area with the blue background known as the ZipSystem. However, I’m getting a lot closer–having now proved all but one of the components within these two aggregate components.

Indeed, if you just judge from the table (and figure) above, I’ve got the entire CPU periphery proven, just not the core module itself or the two container modules–the zipsystem, or the zipbones. As for the main CPU component, I’ve started working on it–but haven’t tried it to see how far I could get. My biggest fear there is that there’s some pipeline bug still lying dormant within the CPU that I will only discover via formal verification.

I’ve certainly found several subtle bugs along the way. For example, just the right sequence of commands and the DMA controller would try to initiate a bus transaction of zero length–violating a primary assertion. As another example, that simple count-down timer would “break” if just the right series of commands were given to it. Or worse, the (soon to be integrated) MMU component would sometimes place the last physical page address on the bus instead of the one appropriate for the current bus request.

I’m hoping to present these proven components here on this blog in time. If you are interested in the proofs before then, you should be able to find some of those proofs in the development branch of the ZipCPU repository, otherwise feel free to write if you don’t find what you are looking for. It will take me some time to integrate these components and then to write the ZipCPU getting started “how-to” instructions, since I want to make certain that the test benches within the ZipCPU repository still work (I think I broke one or two), that the CPU test within the ZBasic repository continues to work, as well as making certain that the CPU still builds within both Xilinx’s ISE (i.e. the XuLA2-LX25 SoC repository) and Vivado (i.e. either the VideoZip or the OpenArty repository).

Getting these components to build for five separate synthesis engines, Verilator, yosys, ISE, Vivado, and (now hopefully) Quartus, has become such a hassle, that I’ve asked among my friends in the OpenRISC world for some ideas to help, and I’ve been told that FuseSoC can handle testing builds for all of these different synthesis tools with one configuration. I think I’m going to need to try that.

Other Components

I’ve also slowly been formally verifying many of the peripherals I’ve been working with. Below, therefore, are some other important components that I’ve managed to formally verify as well:

Project Component Purpose Status
XuLA2-LX25 wbsdram SDRAM controller Proven
wb2axip wbm2axip Pipelined WB to AXI converter Proven
vgasim llvga Low-level VGA Controller Proven
wbpmic wbsmpladc Simple WB A/D Controller Proven
  smplfifo A/D Converter’s FIFO Proven
  smpladc SPI based A/D Converter Proven
wbuart ufifo Generic FIFO for serial ports Proven
wbuart txuartlite Bare bones serial port transmitter Proven
dspfilters lfsr Generic LFSR Proven
dspfilters delayw Signal delay module Proven
qspiflash llqspi Low level QSPI flash driver Proven

Each of these components has a story to tell. For example, I found the subtlest of bugs in the SDRAM memory controller, a bug that in rare cases would have caused the memory controller to read or write the wrong memory address (i.e., the right column but the wrong row). I’ll admit, I was a bit surprised to find this, as I’ve now been using this memory controller for years now and haven’t hit that bug. (Not all of these proofs have been pushed to their respective repositories yet …)

All of the items listed above are candidates for future blog articles–both the ZipCPU and its components as well as the peripherals listed above. Not only do I think they might be of interest to some, but blogging about them will also give me the opportunity to clean up the code a bit following this last mad dash to prove the ZipCPU.

Oh, by the way, if you want to get started with the ZipCPU before I write my getting started article, you can find some simple getting-started instructions here–just to get you going until I write up something prettier.