Formal is the New Normal: Enabler to Single Tape-out Design Qualification

With increasing complexity and size of modern-day designs, verification and validation has become the long pole of the design cycle. The current ratio of verification engineers to designers is 5:1 for most processor design projects, and the cost of verification is 70% of a design verification budget. Even so, the 2020 Wilson Research Group report from Siemens EDA’s Harry Foster points out that 68% of ASICS go through a re-spin and 83% of FPGAs do not work the first time. Simulation, which is widely used for pre-silicon verification of designs, suffers from the inherent problem of incompleteness, since its coverage is as good as the number of testcases written and can miss corner-case bugs, affecting verification closure. Typically, the missed bug scenarios get caught late in the cycle, leading to days of debug effort spent by multiple engineers and teams, and leading to costly ECOs. Formal verification is a verification technology which can check the design correctness exhaustively, by mathematically representing the design state space and then traversing the entire state space to flush out issues. Formal verification has evolved from being a very specialized niche technology being practiced by a select few experts to a critical component of the verification cycle, left-shifting the design verification cycle by days and months and flushing out critical corner-case issues which are not detected even after days of simulation. If a design is proved functionally correct through formal, it acts as a guarantee of absence of bugs, eliminating the chances of ECOs for the same.

The main bottleneck of formal is the state space explosion problem, making it difficult to scale to larger and more complex designs. For effective usage of formal, the trick of the trade is to identify smaller control-intensive design blocks which are amenable to closure with formal. Whereas, for larger designs at subsystem/SOC levels, a verification methodology/flow is required to be developed by utilizing the strengths of formal to aid sign-off where advanced techniques, heuristics and expertise are still needed to harness the complexity challenges. Another very important focus area is of course improving and fine-tuning the algorithms and the intelligence inside the formal tools so that convergence of hard-to-prove properties can be improved. Another direction is the different verification problems which can be targeted using formal, like clock domain crossing, low power, security, functional safety, Linting checks, connectivity, sequential equivalence checking and the like and making the formal flow push-button for such targeted applications.