The Seven Steps Of Formal Signoff

“Signoff” may be the most exciting—and frightening—word in semiconductor development. After many months, or even years of team effort, committing a design to silicon fabrication is indeed an exciting and rewarding event. But, there’s often significant anxiety involved as well – if any missed issues result in having to “turn” the chip, the increased costs and time-to-market delay can be staggering. Accordingly, each stage in the development process must have clearly defined criteria for its contribution to final signoff. Formal verification is no exception, and this article discusses seven critical steps that must be taken to achieve the necessary confidence for formal signoff.

Formal verification involves mathematical analysis of the register transfer level (RTL) design and user-specified properties about the design. Assert properties (assertions) specify intended design behavior, assume properties (constraints) control the analysis, and cover properties measure how well the analysis exercises the design. Unlike simulation or emulation, formal is exhaustive and does not rely on a testbench or test vectors. It is a powerful technology, but it is important for users to keep in mind that the results are only as good as the properties being analyzed. Thus, the seven steps of formal signoff focus on ensuring that the number and quality of the properties are sufficient and on providing a quantifiable measure of functional verification completeness.

The first step is a thorough review of the test plan and the specification. Design and verification engineers write the properties based on design features identified in the test plan. If the plan does not accurately reflect the intended functionality in the spec, then the properties are likely to be incomplete. This review is typically performed by the verification team, although design engineers may be involved as well. Designers are required for the second step, in which they review the properties and the formal results. They know their own RTL code and the intended behavior, so have deep insight into which aspects of the design should be checked by assertions and covered during verification. Both these review steps may occur multiple times over the course of a project as the design and properties evolve and formal runs are completed.

The goal of formal verification is to mathematically prove that all assertions are correct while covering the complete design. Since this depends so much on the properties, the remaining five steps in formal signoff involve answering key questions about the interaction between the design and the properties:

• Are there enough properties to check and cover all the design?
• Are there any invalid proofs due to incorrect constraints?
• Has the design been analyzed at sufficient sequential depth?
• Which portions of the design have truly been verified?
• Can the assertions catch all possible bugs in the design?

The VC Formal next-generation formal verification solution and supporting applications (apps) from Synopsys have the power to answer these questions with minimal user effort. For example, VC Formal can automatically perform a quick analysis to trace backwards from each assertion or cover property to see what parts of the design are in its cone of influence (COI). This provides an answer to the first question, although later steps provide deeper analysis within each COI. The key value at this stage is identifying any registers, inputs or outputs not within the COI of any assertion, which means that they are not being verified at all by formal analysis. Knowing the specific verification holes is excellent guidance for the user to determine which additional assertions are needed.

Figure 1: Quickly tracing the cones of influence.

The fourth step addresses the concern that over-constraining may mask errors in the design. If the constraints are incorrect, then formal analysis might not be considering some of the legal design behavior. If this behavior is involved in triggering a bug that can be caught by an assertion, the bug will be missed, and the proof of the assertion is invalid. VC Formal performs over-constraint analysis to find unreachable code due to constraints. Any behavior in this code that could trigger a bug will not be considered until the user adjusts the constraints to make the portion of the design reachable. The analysis reports exactly which constraints affect which parts of the design, showing the root cause of the unreachability and making it much easier for the user to perform the necessary adjustments.

Formal verification is an exhaustive technology, and the preferred goal on any chip project is to achieve a full proof of all assertions. This is a compute-intensive problem, and on large designs with complex properties it may take a long time – or require a large amount of memory – to get a full (unbounded) proof for every assertion. VC Formal applies algorithms that can generate bounded proofs and reports the number of cycles (depth) for each such proof. It also provides information on the sequential depth of the overall design to help the user decide whether the achieved bounded proof provides high confidence (though not certainty) that the design is correct. This answers the third key question, and the user can request deeper bounded proofs if a sufficient level of confidence has not yet been attained.

The sixth step tackles the question of which portions of the design have truly been verified. The COI approach is fast but overly optimistic in judging assertion density and quality. Some registers or inputs within a COI may not actually be involved in the proof (full or bounded) of the related assertion. VC Formal performs formal core analysis on a subset of each COI to determine which registers or inputs are required for the proof. These can be mapped on to coverage metrics and VC Formal can generate a coverage database for the Synopsys Verdi Automated Debug System. Within Verdi’s coverage viewer, the user can merge results from simulation and formal to assess the complementary verification provided by the two techniques.

Figure 2: Performing formal core analysis and providing coverage results.

Formal core analysis is more precise than COI, but it cannot answer the final question for formal closure. It can tell the user that something about a register has been checked, but not if everything has been checked. The final step combines VC Formal with the Synopsys Formal Testbench Analyzer (FTA) app to provide the most precise assertion metrics. The FTA app inserts faults (mutations) into the design with Synopsys Certitude functional qualification system to model the types of bugs typically found in RTL code. Examples includes a variable or expression stuck high or low, an incorrect value specified (such as 0 instead of 1) and an incorrect operation specified (such as addition instead of subtraction). The analysis determines whether each fault is detected by any of the assertions. Any undetected faults are highlighted clearly in the code to guide the user on what assertions should be added.

The seven steps of formal signoff establish a methodology that answers the key questions about formal analysis and the properties it leverages. Users of Synopsys VC Formal can apply these steps automatically at appropriate points in a chip development project to get maximum value from the technologies and ensure that there are no verification holes. More information on the formal signoff flow, including a demonstration of VC Formal, is available in a webinar.