Formal Verification Posts

  • Examining Xilinx's AXI demonstration core

    Vivado has a wonderful capability, whereby it can create a AXI4 IP core for you to build a design off of. Sadly, the core generated by Vivado 2018.3 doesn't pass formal verification. Let's look at some of the problems with it today.

  • The most common AXI mistake

    After formally verifying several AXI-lite slaves, one bug stands head and shoulders above the rest as the most common bug

  • Using Sequence Properties to Verify a Serial Port Transmitter

    Formally Verifying a serial port makes a great example of both the good and bad about SystemVerilog sequences, and how you can still work around the bad with SymbiYosys

  • Building a custom yet functional AXI-lite slave

    Some time ago, I wrote on this blog about how to verify an AXI-lite slave, showing along the way how Xilinx's demonstration slave wouldn't pass a verification test. Instead of illustrating the problem again, let's take a moment to examine how to build an AXI-lite slave that will not only work, but have twice the throughput.

  • Using a formal property file to verify an AXI-lite peripheral

    A file of formal properties defining an interface is worth gold: you can get a strong guarantee that your code will conform to the interface if it passes a formal verification step using the interface. Even better, one such file, used across an enterprise, can guarantee that all of the cores within the enterprise are interface compatible.

  • Makefiles for formal proofs with SymbiYosys

    Building a make script to verify multiple configuration options using SymbiYosys can be done very easily. Let's take a quick look and see how that might be done.

  • Swapping assumptions and assertions doesn't work

    Some time ago, I blogged about how to go about aggregating subcomponents together into a larger design. While I've used the technique often with great success, this article shares a counter example that renders the approach invalid.

  • My design works in simulation, but not in hardware. Can formal methods help me?

    Formal methods are traditionally viewed as a design tool to be used before implementation. Today, let's take a peek at a recent example where formal methods were able to help me after implementation.

  • How to build a SPI Flash Controller for an FPGA

    I've now written several (Q/D)SPI flash drivers, and just recently had the opportunity to build another. Here I present the design decisions, the design, and even the formal verification of this new core.

  • Why I like Formal: the ZipCPU and the ICO board

    Recently, I had to move logic from one clock to another in order to fit the ZipCPU onto the ICO board. Having a set of formal properties for the ZipCPU, properties that covered this change, gave me a strong confidence when making the change that the result would still work.

  • What does Formal Development look like in Practice?

    I just built a basic, simple SPI controller last night, using formal tools along the way. Care to read what the development was like?

  • Formally Verifying Memory and Cache Components

    There's a necessary but basic trick necessary when formally verifying something that acts like or interacts with memory, and it's not all that hard to do. In this article, I'll present that basic trick and show how to formally verify a block RAM device.

  • Crossing clock domains with an Asynchronous FIFO

    A two or three clock synchronizer works great for passing small amounts of information across clock domains. If you need to pass more information, such as a full data stream, you will need an asynchronous FIFO. This article examines the Asynchronous FIFO designed by Cliff Cummings, applying formal methods to it to see if it truly maintains the properties he discusses.

  • Formally Verifying Asynchronous Components

    There's a very small bit of trickery required to formally verify an asynchronous design using yosys. Once you know the trick, it becomes easy to set up the properties necessary to formally verify any asynchronous design. In this article, we'll demonstrate this principle by formally verifying a clock switch.

  • Aggregating verified modules together

    Aggregating multiple modules together to formally verify a larger whole can be a very difficult challenge. While I am by no means the expert on this topic, I can at least share some lessons I've learned myself.

  • ZipTimer: A simple countdown timer

    When learning Formal Verification, it helps to start with the simplest designs possible. The ZipTimer is just about that simple: it is nothing more than a programmable countdown timer. More than that, though, it's a usable and critical component of the ZipSystem. Today, let's examine that timer and then formally verify it.

  • Formally Verifying an Asynchronous Reset

    It's one thing to synchronize reset logic within your code, its another to formally prove that your reset synchronizing logic works. This article takes a look at an example reset synchronizer, and then applies SymbiYosys to formally verifying that it works.

  • Will formal methods ever find a bug in a working CPU?

    I've now turned my attention to formally Verifying the ZipCPU. Having used the ZipCPU for several years, do you think I'll find any errors within i?

  • Pipelining a Prefetch

    We've already discussed the simplest of the ZipCPU's several prefetch modules. Today's discussion focuses on another module that's nearly as simple, but yet can achieve much better performance.

  • Is formal really all that hard?

    There seems to be a myth that formal verification is very difficult, and that it is only used by the smartest digital designers. Let me take a moment in this article to dispel that myth: If you are smart enough to do digital design, then you will appreciate the benefits of formal verification

  • An Exercise in using Formal Induction

    Passing N steps of a formal bounded model check isn't nearly as hard as proving a design works for all steps. This post explores some of the differences, and offers some explanations for those new to formal methods.

  • Updating ZipCPU files

    I'll admit, I've enjoyed formal methods so much I've started formally verifying much of the ZipCPU repository. Here's a quick status update of what's been accomplished.

  • Building a prefetch module for the ZipCPU

    The pre-fetch module is one of the fundamental components of any CPU. It is responsible for fetching instructions from memory. The ZipCPU prefetch is also an example of a Wishbone master, something worth looking at again in and of itself. This post adds a twist, though, to those two topics in that we'll also formally prove that this prefetch algorithm properly accesses the Wishbone bus.

  • Building Formal Assumptions to Describe Wishbone Behaviour

    The most critical component of any bus based system, such as a System on a Chip (SoC), is the bus interface. One failure of this interface can easily lock up the entire system. This post examines the Wishbone bus interface, and presents some formal properties that can be used to verify that a Wishbone master works.

  • My first experience with Formal Methods

    I've just started trying formal verification methods based upon yosys and yosys-smtbmc this week. As a result, I've now found several subtle bugs within my FIFOs, things that I would never have found otherwise. This post shares some of my initial thoughts and experiences, as well as providing a short primer to the method.