Traditionally, the price of formal methods has limited their use to small teams of verification engineers within large corporations. Today, SymbiYosys lowers the price of formal verification tools to the point where every RTL developer can use them.
The course teaches formal verification from the basics through bounded model checking and induction steps. Specific topics discussed include dissimilar clocking, abstraction, invariants, arbitrary values, and more. Examples will be drawn from counters, SPI interactions, SDRAM controllers, cache implementations, peripheral bus interaction, and more.
This course can be booked for corporate training on-site. Please contact me for details.
- The ZipCPU
A fully functional, fully pipelined, 32-bit CPU designed for resource constrained FPGA environments. Although designed to be powerful enough to run Linux, a Linux port has not yet been written. Many of the projects that follow use this CPU.
If you are interested, consider reading "A Quick Introduction to the ZipCPU's Instruction Set", or "Instructions for building the GCC-based toolchain".
Recent developments on the ZipCPU have included the development of both a data cache and an MMU. While the data cache has been (optionally) integrated, it depends upon an external file to tell it what address regions are cachable and which ones are not. An upgraded version of AutoFPGA now provides this information. The MMU has yet to be integrated.
- ZipCPU systems: The following are fully built, full featured systems for
which the ZipCPU has been placed inside
This project is in the middle of a massive rewrite to make it compatible with AutoFPGA. Part of the purpose of this rewrite is to handle the flash controller found on the newer Arty A7 boards. Significant progress has been made, and the new design builds, however not all of the component interfaces work yet.
While the original version of OpenArty required a PModOLEDrgb, a PModUSBUART, a PModSD(card), and a PModGPS, one of the goals of this newer version of OpenArty is not to be more (re)configurable via AutoFPGA so that it doesn't require these pieces of hardware, and yet may still use other pieces.
While fully functional, this design isn't well documented. It's unique because the debug access point to the device is run from the JTAG port, rather than a UART. The system runs on on both the XuLA2-LX25 as well as the XuLA2-LX9. Let me know if you would like to try this, and I'll help you get started.
This design is also unique due to the presence of a formally verified SDRAM controller within it.
This is a bare bones, minimal ZipCPU system. If you wish to build a ZipCPU system and don't know where to start, this may be just the place. See this post for a discussion on how to get started with ZBasic.
- My original ZipCPU project was built for the Basys3
Sorry, this project doesn't have a cool name. It was my first FPGA project, and one from before I was working on open source projects. One unique feature of this one is that I drive the VGA port from the flash, and so this project can be used to display arbitrary presentation types of images (i.e. static images) on a VGA screen. The VGA simulator from this project has since been posted on github as well.
- VideoZIP is
another system I'm working on. This one, though, is built
entirely via the
program. The goal is to both receive HDMI signals, and transmit
HDMI signals. As an unfunded project, it's not complete. However,
I have managed to get the HDMI receive function working (just not
the save to memory part), and it seems to be working well.
There is also a branch offering RGMII based GbE support which has yet to be merged into the project as a whole. GbE support does work, the Tri-mode options haven't been well tested yet.
- ICOZip, unlike the previous systems is a ZipCPU based system designed for the iCE40 on the ICO board. It can be built using the entirely open source yosys based tool-chain. This is another design built using AutoFPGA. Further, like the S6SoC design listed above, this is also a minimum logic design.
- Digital Signal Processing (DSP) cores
This core generator will create a one of several sine-wave generators in Verilog. These include a 1) table based sinewave generator, 2) a quarter-wave table based sinewave generator, 3) a CORDIC based sin/cosine generator, and 4) a quadratically interpolated sinewave generator. The core generator can also generate a CORDIC based arctangent. By using the core-gen approach, bit widths, precisions, and more are all adjustable/configurable.
- DSP Filters
We've discussed many digital filters on the blog. This repository holds the filters I've presented.
Years ago, I built a tutorial slide deck presenting a piecewise polynomial approach to interpolation. That tutorial is housed in this repository. Since then, I've added several Verilog interpolation implementations as well: nearest neighbor, linear, and quadratic.
- Double Clock FFT
This is an open source, pipelined FFT/IFFT generator. The core generator software will create Verilog code for a fairly generic pipelined FFT. It is very configurable, allowing the user to choose:
- The FFT size, and whether a forward or inverse transform is desired
- Input, output, and internal bit widths
- The bit widths of the twiddle factors
- The number of hardware multiplies used. If there aren't enough hardware multiplies available, the FFT will substitute a firmware multiplication algorithm.
- FFT Demo
This project connects a simulated PModMIC3 to a simulated VGA output to create a scrolling spectral raster display. An upgrade to the version on github uses DDR3 SDRAM (instead of large amounts of block RAM), and an HDMI output.
I have published the code for two PLLs. The one I call a logic PLL may be found in this repository. The logic PLL has the unique feature that it can receive and update within a single clock. The other PLL can be found in the GPS schooled clock code. I have also designed a couple of other PLL approaches that will take more than a single clock. Those should have *much* better performance, but I have yet to port those PLL designs to an FPGA and test them.
- Peripherals which may be used by the ZipCPU
- UART controller
Contains both basic, and fully featured, serial port controllers
Two features make this controller particularly valuable. The first is the four basic UART testing designs in the bench/verilog directory. When starting with any new design, before I know how the board designer labeled the UART wires, I use these basic designs to test them. Once tested, I can usually move quickly to a much larger and more complex design with a debugging bus within it. The second valuable feature is the Verilator UART simulator, which forwards a simulated designs UART ports to a TCP/IP network channel.
- Wishbone based scope
This plus the UART to wishbone bus converter I have might easily be considered the basics of any project I work on. Using this wishbone scope, I have debugged many, many interfaces--some listed here. I would recommend it for anyone interested in incorporating an internal logic analyzer (scope) into one of their projects.
There is an AXI-lite version of the scope in the repository as well.
- QSPI Flash controller
All of these controllers can execute software in place (XIP).
- Hyper-RAM Controller
This is also a work in progress. While it currently passes a formal verification step, it doesn't do so with the actual IO delays involved in using hardware IO pins (yet). More to come.
- Ethernet Packet controller
- I2C Controller
This I2C controller repository contains both a slave and master I2C controllers, each wishbone controlled. It has demonstrated itself via the ability to read and write EDID display information as part of an HDMI project.
- PWM Audio Controller
- GPS schooled clock
This project takes, as input, the PPS signal from a PMod GPS and locks an internal counter to the signal. Using this core, you can record the time events to a precision of less than a fraction of a microsecond.
This project is currently part of my OpenArty project, but I've applied it to other projects of mine as well. Currently, using the crystal oscillator on the Arty and the PMod GPS from Digilent, it can timestamp events within the design to within about 500ns or so of absolute time. I have every reason to believe that, were I able to actually test the algorithm properly using a proper OCXO and (better yet) an external reference clock, then I would be able to measure a much better performance--I just don't have the test setup to try this.
- RTC Clock
This is a very simple, almost beginner, exercise to create a clock in hours, minutes and seconds. It also includes a minutes and seconds count-down timer, a stop watch, and alarm capability.
- SDSPI SD-card controller
In order to use the SD Card on the XuLA board, I needed a SPI based SD-Card controller. While I intend to upgrade this to SDIO in the future, the SPI based controller is still valuable for some designs.
Update: I can now read and write files from/to the SD Card. I hope to post soon about how to build a boot loader in ROM to load either software or a design from an SD card using this controller.
- FM transmitter hack
Just to prove FPGA's are in no ways inferior to Raspberry PI's, this peripheral can be used to turn your GPIO pins into an ad-hoc FM transmitter.
Oled, a controller for the
PMod OLEDrgb display
A special feature of this design is the GTKmm based simulation component, allowing you to visually "see" what the controller would be placing on the screen.
- ICAPE Interface
Xilinx's internal configuration access port provides some very useful features. Getting it running initially, though, was a touch of a challenge. This project captures what it takes in a Wishbone peripheral format.
- VGA Simulator
While not technically a "peripheral that may be used by the ZipCPU", the VGA simulator is a very important part of any graphical development. A not-yet-released version simulates HDMI as well. Using the simulator, you will be able to run your code within Verilator and visualize the output within a GTK window on your computer screen--with no hardware required beyond your desktop machine.
- UART controller
- Projects that are not posted
I am a businessman after all, and Gisselquist Technology, LLC, is in the business of making money. Hence, the following two projects are available for sale to anyone interested.
- High resolution frequency analyzer and synthesizer
We'll discuss this more on this forum as time goes by. For now, the information on the teaser page should be sufficient to gather some interest.
- Universal resampler, sometimes called an Asynchronous Sample Rate Converter (ASRC)
Given any signal into your FPGA, at up to the speed of the controller (100MHz), downsample that signal to any desired rate with 32-bit fractional precision. Alternatively, if you want to upsample, you can upsample your signal and then use this universal resampler to come down to the rate you would like.
What makes this project unique from other resamplers you might use or build is that the aliasing products from the arbitrary resampler are attenuated by a -70dB stop band, making this a high quality resampler implementation.
- GPS processor
The GPS processing approach I have is very unique, and so applies to niche applications. It is not designed for real-time operation, but rather for processing raw captured GPS samples at a later time. This allows an ultra low power receiver to capture GPS samples, which will then be processed later for position and velocity. Test results show a great immunity to both interference and a poor quality signals.
- High resolution frequency analyzer and synthesizer
Most of my projects have been released under the GPLv3 license. They may be built with Verilator without violating this license. Indeed, the license allows you to build your own projects using these components. Sadly, going beyond that limit gets into a legally gray area at this time. I would ask, therefore, that if you wish to publish or distribute this code as part of your own project, that you contact me for a more appropriate license. Hence, if you find this license insufficient for your needs, please contact me and I'll be glad to sell you a proprietary license customized to meet your needs.