Formal Verification Posts

  • 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.