How formal verification works

First, define the condition for generating an alarm with an assertion inside the circuit.
For basic verification items such as FIFO overflows and state machine deadlocks, the tool analyzes your circuit and
Automatically generate assertions.
Other important specifications are defined in assertions by designers and verifiers.

Formal verification tools “understand the logic”, so they backtrace the logic of the circuit to verify whether the logic that meets the conditions is possible.

For example, if pin B of CM4 in Figure 1 becomes “H”, the assertion defines it as a violation (failure).
Formal verification tools understand the logic and can determine that for CM4 pin B to go high, CM3's A pin must go high and the C pin must go low.
Furthermore, it can be determined that pin A of CM1 needs to go low and pin B of CM2 needs to go low.
Now that we have the logic all the way to the input pins, we can see that the testbench for this pattern fails.

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 is similar to simulation and real machine verification, in addition to "complete proof" that verifies all states (assertions are satisfied),
You can do a "falsification" that verifies a malfunction (violating an assertion).

Since the number of combinations of malfunctions is smaller than that of normal operations, "falsification" to examine malfunctions can be verified faster than "complete proof".

It is difficult to prove that the test bench used in simulation covers all combinations of internal states.
Formal verification makes it easy to prove that the phenomenon defined by the assertion "doesn't happen".

Features of Formal Verification

・No need for test patterns ⇒ Designers can verify by themselves from the initial stage of design
・No logic simulation required
・Formal verification is faster than logic simulation
・You can prove that “it does not happen”

Weaknesses of Formal Verification

・As the number of stages increases, the path to the input pin becomes complicated ⇒Assertion analysis on the side close to the output takes time

Logic simulation makes it easy to find defects near the output side, so verification using simulation and formal verification can be used together to reduce verification holes.
Since actual device verification is vulnerable to defects due to unexpected usage, it is effective to combine formal verification with actual device verification.

In addition, formal verification tools include RTL verification such as lint checking, dead code detection, and the ability to automatically generate high-coverage testbenches. Since you can understand the logic, you can perform more advanced verification than ordinary lint checks.