Formal Verification vs Simulation

Simulation and formal verification both look for bugs, but they look in very different ways. Simulation runs the design on chosen inputs and watches what happens. Formal verification reasons about all inputs at once and looks for one that breaks a rule. This article compares the two side by side, shows a bug that simulation almost never finds and formal finds in three clock cycles, and explains why real projects use both.

8 min read | Beginner to Intermediate

What You'll Learn

• Describe how simulation and formal verification each look for bugs
• Explain why a rare input value can hide a bug from random simulation
• List the strengths and the limits of each method
• Decide which method fits a given verification question

How Simulation Looks for Bugs

A simulator runs the design like a real circuit, one clock cycle after another. A testbench supplies the inputs: some are written by hand, many are random. Checkers in the testbench compare the outputs with the expected values. Simulation answers the question: does the design do the right thing for these inputs?

Simulation is flexible. It can run a whole chip, with a processor executing a program, for millions of cycles. It checks the real function of the design, end to end. But it can only find a bug if the inputs happen to lead to it, and if a checker notices it.

How Formal Looks for Bugs

A formal tool does not run the design with chosen inputs. It treats every input as unknown and asks: is there any value of these inputs, in any cycle, that makes a property false? The solver answers that question for all input values together. Formal answers the question: is there any input that breaks this rule?

Formal is complete for the question it is asked. If a failing input sequence exists within the bound, the tool finds it. The price is that the question must be written as a property, and that the tool can only handle designs of limited size, because the problem grows quickly with every register.

A Bug That Simulation Almost Never Finds

Here is a small block that raises an alarm output. The alarm must never be raised in normal operation. But the designer left a piece of debug code in it, which sets the alarm when the 32-bit data input has one special value:

module alarm_unit (input clk, input rst, input [31:0] data, output reg alarm);
  always @(posedge clk)
    if (rst)                       alarm <= 1'b0;
    else if (data == 32'hDEADBEEF) alarm <= 1'b1;   // left-over debug code

  assert property (@(posedge clk) disable iff (rst) !alarm);
endmodule

A 32-bit input has 2 to the power 32 values, about 4.3 billion. A random test that applies a new random value in every cycle hits the special value on average once in 4.3 billion cycles. A typical regression of a few million cycles almost certainly never sees it, and the bug ships in the chip.

The formal tool finds it at once. On the lab engine, the property fails at step 3, with this counterexample:

The tool did not get lucky. It asked the solver whether any value of data sets the alarm, and the solver worked out the only value that does, 32'hDEADBEEF. The size of the input space does not matter to it in the way it matters to random testing.

Side by Side

Where Each One Wins

Formal is strongest for:

• Control logic with many corner cases: arbiters, FIFOs, state machines, handshakes.
• Rules that must hold always: no overflow, no deadlock, at most one grant, no data lost.
• Rare values and rare orderings, like the debug code above.
• Proving that two versions of a design are equivalent, for example before and after synthesis.

Simulation is strongest for:

• Large systems, where the formal problem would be too big.
• Long scenarios, such as booting a processor or sending a whole packet stream.
• Checking that the design does the right thing overall, not only that it follows a list of rules.
• Analog models, software, and performance measurements.

Using Both

Real projects do not choose one method. A common split is:

1. The designer uses formal on a new block while writing it, to catch mistakes in minutes without a testbench.
2. The verification team proves the key rules of the critical blocks with formal.
3. Simulation, often with a UVM testbench, checks the complete function and the integration of the blocks.
4. The same assertions are used in both: in formal as rules to prove, in simulation as checkers that fire when a test breaks them.

The last point matters. An SVA property written for formal also works in a simulator. Writing it once gives value twice.

Running It in ChipVerify Lab

The lab example writes the rule of the alarm unit in the form that the open-source engine accepts:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init) assert (!alarm);
`endif

The counterexample is short, so it fits in the free depth of 10 cycles.

Common Mistakes