SupportFormal Verification Posts
-
My Personal Journey in Verification
I've now gone from hardware-only verification, to simulation, through formal verification, to automated test suites. This article attempts to discuss why I've used all these steps together with some of the lessons learned along the way.
-
SDIO RX: Bugs found w/ Formal methods
My SDIO controller has now been tested, successfully, via simulation with success. It builds on hardware. What value, therefore, is left for formally verifying it? Let's therefore examine and count the number of bugs found while formally verifying the receive portion of this controller.
-
Measuring the Steps to Design Checkoff
Before delivering a design to a customer, it's important to have a strong confidence it will work. Prior to that time, it's important to know how much time and work remain in the project. In this article, I'll demonstrate a tool I've now used with great success for that purpose.
-
Ultimate Logic
Logic can be used to prove that certain assertions must follow from the given assumptions. How then shall the assumptions be validated? What about the assumptions behind the assumptions?
-
A fun Friday evening--verifying an AXI-lite slave
Can an AXI-lite slave design be formally verified, from scratch, while others look on?
-
Moving values and strobes cross clock domains
Let's build a two-phase clock-domain crossing algorithm to move words from one domain to another, beating our prior four-phase method in performance and logic.
-
Building a Downsampling Filter
A digital downsampler is a combination of both a digital filter and an every Nth element selector. It's basic. Formally verifying it, perhaps not quite so basic.
-
I have a brand new piece of IP. How shall I verify it?
Verification doesn't begin once a design is complete. It needs to begin long before that, ideally before the design is ever simulated in the first place
-
Four keys to getting your design to work the first time
No, it's not a magical cure, just a general observation: there are four key pieces to verification that come back over and over again in designs that just work the first time
-
Building a Protocol Firewall
A bus fault isolator can be a very useful tool for debugging an AXI interaction within an active design. Once the bus faults and the design locks up, further debugging is a challenge. However, if a fault isolator can keep things from locking up and perhaps even reset the quarrelsome component following a fault, then finding the bug gets a lot easier.
-
A Histogram Gone Bad
I took my working histogram component, and placed it into a full design. It didn't work. Let's take a look at what happened.
-
Using a Histogram to Debug A/D Data Streams
Histograms are an important part of debugging a data channel. Let's take a look at some pictures, and then discuss how to go about implementing one
-
Formally Verifying a General Purpose Ultra-Micro Controller
Let's look at a basic, scripted microcontroller--the simplest around. Understanding how to formally verify something this simple offers a lot of lessons for verifying something more complex.
-
Is formal verfication enough, or is simulation required?
This article captures four stories I tell of bugs found and caught, two after only using simulation and two after only using formal, in an attempt to answer whether or not I could've verified with formal alone or for that matter with simulation alone.
-
AXI Verification, the story so far
After learning how to verify AXI modules, it's now time to discuss some of the reality of what's going on in the industry.
-
Just how long does a formal proof take to finish?
Formal methods are exhaustive, so just how long does it take to prove something? Examining a body of nearly 900 proofs, it's not that long.
-
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.