Formal verification

Others have gone here before me, and now it is my turn!

Formal verification is a tool for verifying the correctness of your implementation. Traditional verification strategies have relied on hand-crafted testbenches to provide stimuli to the DUT. Formal verification aims to automate that process. In my view these two approaches (testbench and formal) supplement each other, rather than replace each other.

Installing the tools

I've written a separate document with a guide on how to install all the necessary tools.

Doing formal verification in VHDL

To use formal verification with VHDL, we need to learn a new language PSL. The VHDL file is augmented with verification commands like assert, assume, and cover. Furthermore, the SymbiYosys tools must be started with some additional command line parameters. This is demonstrated in the below examples.

Example designs using formal verification

• One Stage Fifo. This is a kind of "hello world" of formal verification.
• One Stage Buffer. Another simple but useful module.
• Two Stage Fifo. Small FIFO useful for timing closure.
• Two Stage Buffer. Small FIFO useful for timing closure.
• Pipe_Concat. Concatenate two elastic pipe streams.
• Wishbone memory. This is to learn about the wishbone bus protocol.
• Fetch. The first "real" module. This is a simple instruction fetch module for a CPU.
• Fetch2. A second (more optimized) implementation of the instruction fetch module.

Example puzzles using formal verification

• Fox, Goat, and Cabbage. This uses formal verification to solve a well-known puzzle.
• Rubik's 2x2x2. This uses formal verification to solve Rubik's 2x2x2 cube.

Other resources

• This video gives a nice introduction to formal verification, including a lot of small and easy examples.

• This video-series gives a more detailed tutorial for getting started with formal verification.

• Robert Baruch has made a video series on building a 6800 CPU using nMigen and applying formal verification in the process. This was the first time I heard about formal verification, and has been a great inspiration for me.

• Charles LaForest has compiled a huge resource on VHDL design elements. There is no formal verification, but this website is a good resource, with detailed explanation of each module.