What Is Formal Verification?

The so-called formal verification refers to a mathematically complete proof or verification of whether the circuit's implementation scheme actually implements the functions described in the circuit design. Formal verification methods are divided into equivalence verification, model verification, and theorem proof.

In the formal verification, it is necessary to determine which level of the circuit is tested correctly. Use the model check method to see if the two circuits are consistent in description.

1. Logic verification of combinational logic circuits

For combinational logic, there is no status register, and its output value Z [t] does not depend on the previous input value X [ti] (1it). In this case, just prove that the output vector is the same for each input vector. There are two types of methods in the field of combinatorial logic verification.

(1) Conversion to a single abstract model for comparison. By comparing the structure of a single representation, we conclude that its function is equivalent. In the worst case, the Boolean function is positive, which means that as the number of inputs increases exponentially, its excessive memory requirements limit the general

Formal verification methods include equivalence checking, model checking, and theorem proof. Formal verification is mainly used to check conformance to a given specification while covering all possible inputs. The formal methods of SoC verification are mainly equivalence check and model check.

Model checking is mainly to check whether the RTL code meets some characteristics specified in the specification. When specifying these features, a feature specification language is generally used, and currently an assertion-based verification language is also commonly used. Because this method can check whether all possible situations in the design meet the specified characteristics without the need for simulation, this method will not miss any boundary conditions.

The equivalence check is mainly to check whether the two gate-level netlists are consistent, to ensure that the function of the circuit will not be changed after the netlist is processed, or to ensure that the netlist can correctly implement the functions described by the RTL code, or to ensure that the two RTLs The description logic is consistent. The equivalence check checks the equivalence of two descriptions by comparing them. The equivalence check tool reads the two designs into memory and uses a formal data algorithm to analyze each other's data structures for comparison. As long as all output pins of the two designs have the same function as each register or latch, the functions of the two designs are considered equivalent. It is mainly used to find defects in implementation, not defects in design, and inspection.

The advantages of formal verification are as follows:

(1) Formal verification is to verify all the possible descriptions of the specified description, and the coverage rate reaches 100%.

(2) Formal verification technology uses mathematical methods to directly compare the circuit to be verified with the functional description or reference design, without the need to develop test incentives.

(3) The verification time of formal verification is short, errors in circuit design can be found and corrected quickly, and the design cycle can be shortened.

Formal verification mainly verifies whether the code functions of each stage in the digital IC design process are consistent, including verification of RTL code before synthesis and netlist after synthesis, because today the scale of IC design is getting larger and larger. If gate-level netlists are dynamically simulated, , Which can take a long time, and formal verification can complete a large verification in just a few hours. In addition, because the clock tree synthesis is done after the layout, the insertion of the clock tree means that the original netlist entering the layout tool has been modified, so it is necessary to verify that it is logically equivalent to the original netlist. ^[3]