What Is Formal Verification?

Formal verification is a way of checking a hardware design by reasoning about it mathematically instead of running tests. You write down rules that the design must always follow, called properties, and a formal tool searches through every possible input sequence to find one that breaks a rule. This article explains the idea in plain words, shows a first property, and introduces the tool that ChipVerify Lab uses.

10 min read | Beginner to Intermediate

What You'll Learn

• Explain what formal verification checks and how it differs from running tests
• Describe what a property, a pass and a counterexample are
• Read a first property written in SystemVerilog Assertions
• List the limitations of formal verification
• Say what the formal engine in ChipVerify Lab can do

The Problem With Tests

When you verify a design by simulation, you write a testbench. It drives inputs into the design, cycle by cycle, and checks the outputs. If the outputs are wrong, the test fails and you have found a bug.

The weak point is the word "drives". The testbench only drives the inputs that you, or a random generator, chose. A design with a few inputs and a few registers can receive an enormous number of different input sequences. Even millions of test cycles try only a small part of them. If a bug hides behind an unusual sequence that no test produces, the simulation passes and the bug goes into the chip.

Formal verification turns the problem around. You do not choose the inputs at all. You only say what must always be true, and the tool looks for any input sequence that makes it false.

Properties: Rules the Design Must Follow

A property is a rule about the behavior of a design, written so that a tool can check it. Some examples, in words:

• A counter that counts from 0 to 5 never shows a value larger than 5.
• A FIFO never accepts data when it is full.
• An arbiter never gives the grant to two requesters at the same time.
• After a request, an acknowledge comes within 4 clock cycles.

These rules are written in a language that the tool understands. The standard language is SystemVerilog Assertions, SVA, which is part of SystemVerilog. Here is the first rule of the list as SVA, for a counter with the output q:

assert property (@(posedge clk) disable iff (rst) q <= 3'd5);

Read it from left to right:

• assert property: this is a rule that must always hold.
• @(posedge clk): check it at every rising edge of the clock.
• disable iff (rst): do not check it while the reset is active.
• q <= 3'd5: the rule itself, the counter value is at most 5.

That one line replaces a whole family of tests. It does not say which inputs to apply. It says what must be true for all of them.

Two Possible Answers

A formal tool takes the design and the properties, and gives one of two answers for each property:

• Pass. The tool found no input sequence that breaks the property. Depending on the method, this holds for every sequence up to a certain number of clock cycles, or for every sequence of any length. Chapter 5 and Chapter 6 explain the difference.
• Fail, with a counterexample. The tool found an input sequence that breaks the property. It gives you that sequence as a waveform, cycle by cycle, which you can open like a simulation result. This waveform is called a counterexample, because it is an example that goes against your rule.

The counterexample is the most useful thing a formal tool produces. It is a short, exact recipe for the bug, often only a few cycles long, with no unrelated activity around it.

A First Example

Here is a small counter that is meant to count from 0 to 5 and then start again at 0, for example to count the tens of seconds of a clock:

module mod6 (input clk, input rst, input en, output reg [2:0] q);
  always @(posedge clk)
    if (rst)     q <= 3'd0;
    else if (en) q <= (q == 3'd6) ? 3'd0 : q + 3'd1;   // bug: should be 3'd5

  assert property (@(posedge clk) disable iff (rst) q <= 3'd5);
endmodule

The designer made a small mistake: the counter wraps at 6 instead of 5, so it shows the value 6 for one count. A simulation finds this only if a test runs long enough with en high and someone checks the value. The formal tool finds it by itself. On the lab engine it reports a failure at step 8 and gives this counterexample:

The tool chose the inputs: a reset in the first cycle, and then en high long enough for the counter to climb to 6. Nobody wrote those inputs. With the wrap value corrected to 5, the same run passes.

Why It Is Called Formal

The word formal comes from mathematics, where a formal proof follows exact rules. The tool turns the design and the property into a mathematical problem: is there a sequence of input values for which the property is false? A program called a solver answers that question. It does not try the sequences one by one, which would take forever. It reasons about all of them at once. The article about how a model checker works shows the idea.

Formal Verification in ChipVerify Lab

ChipVerify Lab has a formal engine built from open-source tools: SymbiYosys, which reads the design with Yosys, and three solvers, bitwuzla, boolector and z3. It runs bounded model checking. That means it checks every input sequence up to a number of clock cycles that you choose, called the depth. The depth limit is 10 cycles on the free tier and 100 cycles with PRO. When a property fails, the lab shows the counterexample as a waveform.

Limitations of Formal Verification

Formal verification is exhaustive, but only inside some clear limits. Knowing them is as important as knowing its strengths, because a pass outside these limits means nothing.

• It checks only the properties you write. A rule that nobody wrote down is never checked. If the properties miss an important behavior, a design can pass every formal check and still be wrong. Formal is only as complete as its list of properties.
• It checks only the inputs your assumptions allow. Assumptions tell the tool which inputs are legal. An assumption that is too strict removes real input sequences from the search, and a bug that needs those inputs is never found. In the worst case a wrong assumption makes every property pass without checking anything.
• The design must fit in the tool. Every register doubles the number of possible states. Large blocks, wide arithmetic such as multipliers and floating-point units, big memories and long counters can make a formal run very slow or impossible to finish. Formal is used on blocks of moderate size, not on a whole chip.
• A bounded check stops at its depth. Bounded model checking, which the lab uses, only looks at a fixed number of clock cycles. A bug that needs more cycles to appear is not found. A full proof for any number of cycles is possible, but it does not always finish, and then the result is inconclusive.
• It works on the logic model only. Formal reasons about the 0 and 1 values of the RTL. It does not check analog behavior, the timing of real gates and wires (that is the job of static timing analysis), power, or clocks that drift against each other. It also cannot say whether the specification itself is what the customer wanted.
• It takes skill. Writing good properties and assumptions, and reading counterexamples, is a skill of its own. A beginner can start in minutes, but proving a complex block can take an expert days or weeks.

These limits are why formal and simulation are used together, each where it is strongest. The article about formal verification vs simulation compares them in detail.

Running It in ChipVerify Lab

The open-source front end of the lab does not read the concurrent form assert property (@(posedge clk) ...). The lab example writes the same rule in a form that it accepts: an assert inside a clocked always block, placed in an `ifdef FORMAL section so that simulation tools ignore it.

`ifdef FORMAL
  reg init = 1'b1;                                // high only in the first cycle
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);             // start from a reset
  always @(posedge clk) if (!init) assert (q <= 3'd5);
`endif

The assume line tells the tool to start with a reset, and the assert is the rule. The meaning is the same as the one-line SVA property. Chapter 2 explains each line, and Chapter 3 compares the two forms of assertions in detail.

Common Mistakes