FPGA's Only Talk -Verification- [Part 5] What is Formal Verification...?

In this column, we introduce "FPGA technical information that is surprisingly little known but makes a difference if you know it.
The contents are useful for a wide range of people from FPGA beginners to experienced users, so please stay with us to the end.

Part 5: What is Formal Verification?

In Part 2, I explained about ABV (Assertion-Based Verification). There are two ways to perform ABV

Dynamic verification by logical simulation
Static formal verification

In this article, we will introduce the latter, formal verification.

To perform formal verification, use a formal verification tool that understands "assertions" and "circuit logic.
This tool does not require "test patterns," "simulation," "output waveform monitoring," or "expectation matching," and is easy to operate.

How Formal Verification Works

First, the conditions for generating alarms are defined by assertions inside the circuit.
For basic verification items such as FIFO overflow and state machine deadlock, the tool analyzes the circuit and automatically generates assertions.
Other important specifications are defined in assertions by the designer or verifier.

Formal verification tools "understand logic," so they backtrace the logic of the circuit and verify that the logic applicable to the condition is possible.

　　Figure 1: How formal verification works

For example, an assertion defines that pin B of CM4 in Figure 1 is violated (faulty) if it goes "H".
Since formal verification tools understand logic, they can determine that for pin B of CM4 to be "H", pin A of CM3 must be "H" and pin C must be "L". pin A of CM3 must be "H" and pin C must be "L" in order for pin B of CM4 to be "H".
Furthermore, we can determine that pin A of CM1 must be "L" and pin B of CM2 must be "L" in order for this to happen.
Since the logic has been traced to the input pins, we know that this pattern will cause a failure on the test bench.

Conversely, if there is no condition for pin A of CM1 and pin B of CM2 to be "L", we can prove that this failure cannot occur.

Formal verification, like simulation and actual device verification, is not only a "complete proof" that verifies all conditions (satisfies the assertion), but also a "rebuttal proof" that verifies malfunctions (violates the assertion). ", which verifies all the states (satisfying the assertion).

Since malfunctions have fewer combinations than normal operations, "disproof" to check for malfunctions is faster than "full proof.

While it is difficult to prove that the testbench used in simulation covers all combinations of internal states, formal verification can easily prove that a phenomenon defined by an assertion "does not occur.

Features of Formal Verification

No test patterns are required ⇒ Designers can verify by themselves from the early stage of design
No need to run logic simulation
Formal verification is faster than logic simulation
Proof of "not happening" is possible.

Weaknesses of formal verification

The more steps, the more complex the path to the input pins ⇒ Assertion analysis on the side close to the outputs takes time

Logic simulation is more likely to find defects on the side close to the outputs, so using formal verification together with simulation can reduce the verification hole.
Since actual device verification is vulnerable to defects caused by unexpected usage, combining formal verification with actual device verification is also effective.

In addition, formal verification tools provide RTL verification such as dead code detection, which is a lint check, and the ability to automatically generate a testbench with high coverage. Since they can understand logic, they can perform more advanced verification than ordinary lint checks.

Know the difference! FPGA Only in FPGA Series

Power Consumption

Verification