The ZipCPU blog has recently picked up a lot of readers in light of my recent on-going work to formally verify the entire ZipCPU.

To all of those new readers, Welcome!.

The ZipCPU blog is dedicated to helping FPGA designers avoid getting stuck in FPGA Hell–a place where your design doesn’t work and you can’t figure out why not. To this end, I’ve presented techniques for simulating your design using Verilator, how to build a debugging bus for command, control, and internal register and state inspection, how to build your own internal logic analyzer, how to use my own wishbone scope, how the VCD file format expresses your logic trace, how to debug a DSP algorithm, network debugging, and more.

Recently I’ve started learning about formal verification, and so I’ve added that topic to my list as well. As a result there have now been several articles on how to formally verify your logic as and after you have put it together, and the value of formal verification.

What you as a reader need to know, however, is that these articles are sponsor supported. If you find this blog valuable, and would like to see it continue, then please consider becoming one of my Patreon Sponsors.

One of the perks of being a sponsor is that I am responsive to the topics my sponsors are interested in.

sponsors. So, here’s a short list of some of the upcoming topics which I think would be fun to post about. If you are one of my sponsors, then please consider yourself invited to contact me and let me know which of these (or other) topics you might be interested in. There is also a more complete list of both past and upcoming topics in the site topics list as well.

So, without further delay, here are some of the topics I am considering writing about in the near future, should the Lord be willing:

  • ZBasic ZipCPU Peripheral: Some time ago, I promised I was going to discuss how easy it was to add a peripheral to the ZBasic using AutoFPGA. I am still fully intending to do this, although I am somewhat struggling to decide what that example peripheral should be–there are just too many possibilities. Feel free to make a suggestion if you would like.

  • Quadratic Sinewave generation: CORDIC sinewave generation is really cool, but it can also be logically expensive within an FPGA. A potentially cheaper algorithm, requiring only two multiplies, would be to apply our quadratic interpolation techniques to generating a cleaner sine wave.

  • Asynchronous FIFO: I have a nice formal proof of Cliff Cummings’ asynchronous FIFO design that I think would be valuable to present as well. Unlike many of my other formal articles, this one requires a formal solution across more than one clock domain, and for arbitrary clock speeds. This will add to the interest and value of it.

  • Ethernet CRC: When I recently built a Ethernet CRC module for the 1Gb Ethernet port of the Nexys Video board, I was surprised at how much formal methods could help simplify the complicated math of a multi-stepping CRC generator. This would therefore be a fun topic to share, as there is a lot of practical information within it.

  • Dual I/O SPI flash: While I am personally quite biased towards a Quad SPI flash implementation, recent events have led me to need to build a Dual I/O SPI flash implementation for a couple of logic challenged implementations. This means that this controller should be simple enough to both present and understand, and makes a nice blog topic

    • TinyFPGA: I’m also building a TinyFPGA BX design using the ZipCPU, and would love to blog about this design. Yes, the ZipCPU does fit nicely on that board with room to spare (when properly trimmed), however my minimal flash controller needed to be redesigned, and my C++ flash simulator needed to be adjusted to get this to work. Once I’ve finished verifying that I can program and run the ZipCPU on this board, then it would be fun to describe my experiences. Because of the dependence upon the flash controller, however, this post would follow the discussion of the Dual I/O SPI flash design.

  • Some Simple Formal Verification Proofs: It might be nice to return to our (event) timing control solutions post, and take a new look at them in light of formal verification. For example, how would you verify that a timer provides you with the right number of clock ticks, or how would you speed up an otherwise exceptionally long proof.

  • Prefetch with Cache: The ZipCPU has a 1-way instruction cache that would be fun to present, and would also conclude our discussion of prefetch methods.

  • Data Movement: One of the sad realities of FPGA work is that its not all about data transformation. There’s a lot to be done in data movement as well.

    The ZiPCPU contains a DMA controller that can be set up to automatically move data from one place to another within any wishbone based design. This component, and its formal properties would be useful to many of my readers.

  • Abstraction in Formal Verification: The recent ZipCPU verification work depends heavily on formal verification concepts of abstraction and invariance. Both techniques are useful when trying to break a complicated design, such as a full CPU, down into its subcomponents.

    This article would present abstraction. In short, abstraction is based upon the statement that if A implies B, then A and C must also imply B. The figures and outline of this lesson would be taken from the formal verification course I’ve put together for Symbiotic EDA.

  • Invariance in Formal Verification: Invariance is a second very powerful tool that can be used to simplify the formal prove of a component. Put simply, if you can prove the A is true, you no longer need to prove A anymore. The difference over what can, and cannot, be proven using this technique can be drastic.

    The figures and outline of this lesson would also be taken from the formal verification course I’ve put together for Symbiotic EDA, just like the proposed abstraction post discussed above.

  • More filtering: We left our discussion of filtering incomplete, and so I’d still like to come back to demonstrate both symmetric and halfband filters.

  • Dhrystone: Also on my list of items to discuss is Dhrystone, the outdated-yet-still-useful CPU bench mark. For all of you who are interested in comparing your CPU’s performance against Dhrystone, this article would take a quick look at how Dhrystone can be run within a Verilator simulation, and how I’ve gone about interpreting the results.

  • Synchronization: One common problem in digital signal processing is the “two-clock” problem where data comes into the algorithm on one clock, and yet needs to be output on the edges of an unrelated clock. Now that we’ve spent some time with interpolation, as well as how to build a simple PLL module, it only makes sense that we would connect these two concepts to be able to synchronize two data streams.

  • Generating an Arbitrary Clock Signal: I also have a simple design component that can be used to generate a clock signal at an arbitrary frequency, without requiring any additional clock chips. (The FPGA still needs its input clock.)

  • Building a HyperRAM controller: HyperRAM is a powerful RAM communication protocol. Unlike DDR3 SDRAM, building a controller for HyperRAM doesn’t require undocumented chip features. This article would discuss such a controller, both how to build it as well as how to formally verify that it works.

    If there’s enough demand, a separate article could discuss how to build a simulation component for this device.

If you’ve made it this far, let share this with you: I’m creating today a formal page which will capture all of my formal verification posts. This should make it easier for someone who is only interested in formal verification to find articles that discuss or provide examples of formal verification.

This new topical page joins my prior DSP topical page. However, all articles will remain on the blog’s main page.

Finally, if you are one of my Patreon sponsors, please feel free to contact me at the e-mail address below and let me know which, if any, of these topics you might be interested in. Even better, these are only suggestions. If you are interested in a topic that isn’t listed above, please feel free to share that topic with me as well. Just please be aware that topics not on this list, such as creating a GCC port, might take a bit longer to work up to.

If you are not one of my Patreon sponsors, and yet you find this blog valuable, please consider joining the team! While I have no intention of restricting the blog’s content to subscribers only, your support will help this blog continue into the future.