This post is the second in a series introducing formal verification of hardware circuits in Verilog. Take a look at part 1 for an introduction to what formal is and how to set up a verification flow.

In this article, we will start by verifying a slightly more complex combinational design - an integer ALU - and then introduce a clock to look at how to verify synchronous circuits.

The ALU Design

Let’s create a simple ALU that performs addition, subtraction, bitwise and, and bitwise xor on two 8-bit inputs and produces an 8 bit output (2’s complement). To make the simulation more interesting, let’s write it out logically as two chained 4-bit carry lookahead adders (in real life, this is rarely a good idea as + is simple enough for your synthesis tool to do a good job). I’m doing this only to motivate the fact that your DUT is usually implementing a complex circuit in an efficient way while your formal properties are verifying simple and straight forward properties about your design as succinctly as possible to avoid errors (synthesis isn’t an issue here).

Hi! This post is the first in a series introducing formal verification of hardware circuits in Verilog (and similar hardware description languages). While there are a couple of good resources for formal, especially zipcpu.com, the literature is surprisingly sparse, especially including end to end examples.

In this series, I want to develop an intuition for formal verification from first principles, working up all the way to formally verifying a reasonably complex IP (perhaps a simple processor core) with examples. Lets get started!