Debate over Formal Sign-off vs. Bug-hunting
Formal technologies have been used in many different ways in the industry including automatic formal, formal apps and so on. One of ways of using formal technology is use it for formal sign-off. Oski has developed a Formal Sign-off methodology that covers complete design functionality to ensure 100% correct design behavior according to design spec. This is achieved by addressing all 4 Cs namely Complexity, Constraints, Checkers, Coverage of formal verification testbench that are critical for the formal success. End-to-End checkers are needed for formal to replace simulation to completely verify the end-to-end functionality of the blocks, constraints need to be appropriate so there is no unintentional under- and over-constraints that could lead to missing bugs or false results, most importantly complexity needs to be managed so we can achieve sufficient proof for end-to-end checkers, lastly formal coverage needs to be measured to ensure sign-off. We have deployed Formal Sign-off on different designs with multiple customers and the customers are benefited by first time silicon success.
Figure 1: 4Cs of formal verification testbench
Another way to use formal technology is to use it exclusively to uncover bugs in the design, popularly referred as bug-hunting. Here the formal is used to complement simulation to find additional corner case bugs. The focus for bug-hunting is on targeted design functionality that is error prone:
1) Complex corner cases
2) Where simulation is lacking
3) Where simulation found a lot of issues
The bug-hunting requires writing targeted internal, interface assertions or End-to-End checkers to verify specific functionality. Just like formal sign-off, bug-hunting approach may also need to deal with complexity with Abstraction Models and bounded proof. Even though bug-hunting can be very effective in uncovering corner-case bugs in the designs, it cannot be used for sign-off. The simulation remains the main verification strategy for such design. In contrast, formal sign-off does not require simulation for sign-off. Bug-hunting helps by providing laser sharp focus to zoom into concerned functional area and catch bugs early. But bug-hunting with simulation could still miss some bugs because the exhaustiveness of formal technology is not used to verify the complete design. In comparison, Formal Sign-off can uncover all the bugs in the design.
So, should we always choose Formal Sign-off? The answer depends on factors like the verification goal, scheduled and completeness of the current simulation verification, measured by coverage. If the goal is to catch corner case bugs missed by simulation and schedule is short like couple of weeks, then bug-hunting could be a effective technique. If goal is to achieve 100% design confidence then Formal Sign-off is better choice.