What is Formal Verification in Semiconductor Engineering?

What is formal verification?

Formal verification is an essential part of semiconductor development, but it also requires careful planning, rigorous reviews, and comprehensive metrics to achieve a quantifiable measure of functional verification completeness. By following the steps of formal signoff talked in this article, semiconductor developers can ensure that their designs are correct and quality, and that they are ready for fabrication.

Formal verification is a powerful and essential technique for ensuring the correctness and quality of semiconductor designs. Unlike simulation or emulation, which rely on testbenches and test vectors to exercise the design, formal verification uses mathematical analysis to exhaustively check the design against user-specified properties. These properties can be assertions that describe the intended behavior of the design, constraints that control the analysis, or cover points that measure how well the analysis exercises the design.

Formal verification can find subtle and corner-case bugs that may escape simulation or emulation, and can provide a higher level of confidence in the design functionality. However, formal verification also requires careful planning, rigorous reviews, and comprehensive metrics to achieve a quantifiable measure of functional verification completeness. 

In this blog post, we will discuss the seven steps of formal signoff that can help semiconductor developers achieve this goal.

Step 1: Review the test plan and the specification

The first step is to ensure that the test plan accurately reflects the intended functionality of the design as described in the specification. The test plan identifies the design features that need to be verified and how they will be verified. The formal verification team will use the test plan to write properties that check and cover these features. If the test plan is incomplete or inconsistent with the specification, then the properties may also be incomplete or incorrect.

Step 2: Review the properties and the formal results

The second step is to have the design engineers review the properties and the formal results. The design engineers have deep insight into their own RTL code and the intended behavior of the design, so they can verify that the properties are correct and sufficient, and that the formal results are consistent with their expectations. They can also provide feedback on how to improve or optimize the properties or the formal analysis.

Step 3: Check property coverage

The third step is to check how well the properties cover the design. Property coverage measures how much of the design functionality is specified by assertions and cover points. A high property coverage indicates that the design has been thoroughly checked and exercised by formal verification. A low property coverage may indicate that some design features are missing from the test plan or that some properties are too abstract or too specific.

Step 4: Check proof status

The fourth step is to check the proof status of each property. The proof status indicates whether formal verification has been able to prove or disprove a property, or whether it has reached a limit in terms of time, memory, or sequential depth. A proven property means that formal verification has confirmed that the property holds for all possible inputs and states of the design. A disproven property means that formal verification has found a counterexample where the property fails. A bounded property means that formal verification has only checked the property within a certain scope or under certain assumptions.

Step 5: Check constraint validity

The fifth step is to check whether any constraints used in formal verification are valid. Constraints are assume properties that restrict the input space or state space of formal analysis. They can help reduce complexity, improve performance, and avoid false negatives or false positives. However, constraints must be carefully written and reviewed to ensure that they do not over-constrain or under-constrain the design. Over-constraining may lead to invalid proofs where some bugs are masked by unrealistic assumptions. Under-constraining may lead to invalid counterexamples where some failures are caused by unrealistic inputs.

Step 6: Check sequential depth

The sixth step is to check whether formal verification has analyzed the design at sufficient sequential depth. Sequential depth measures how many clock cycles are needed to reach a certain state or behavior in the design. Formal verification can prove properties at any sequential depth, but it may take longer or require more resources as the depth increases. Therefore, it is important to set a reasonable target depth for each property based on its complexity and relevance. A target depth should be large enough to cover all possible scenarios of interest, but not too large to cause unnecessary overhead.

Step 7: Check functional coverage

The seventh and final step is to check how well formal verification has exercised the design functionality. Functional coverage measures how many cover points have been hit by formal analysis. Cover points are properties that specify interesting or critical states or behaviors in the design. A high functional coverage indicates that formal verification has explored a large portion of the design space and has not missed any important cases. A low functional coverage may indicate that some cover points are unreachable or too difficult for formal verification, or that some scenarios are missing from the test plan.