My last post must have struck a nerve. In this post I ask whether fundamental innovation stalled in formal verification, and I speculate which area the next technological leap will come from. This post received some quite interesting comments. It also brought a counter point by Brian Bailey, partially motivated by his business partnership with Jasper –Brian sits in Jasper’s Technical Advisory Board. Last Friday I had a lively discussion with Rajeev Ranjan (CTO) and Holly Stump (VP Marketing) of Jasper. I am now taking the time to discuss these feedbacks.
My claim is that formal verification has reached a plateau from both the core technology and business point of view.
Yet that does not mean there is no progress! There is a world between creating a brand new technology and using it for an actual working product. This is what the Jasper, Real Intent, Atrenta, OneSpin, and many others are doing, as they creatively use these core technologies to propose new applications.
From the technological point of view, we have experienced steady improvements in many aspects –equivalence checking (EC), sequential verification, abstraction and refinement, etc. The scope of application of formal verification techniques has dramatically increased for the past few years. It has of course benefited from more powerful hardware –faster CPU, larger memory, multi-threading, distributed systems, FPGA. It also benefited from the skilled engineering of the core technologies, to the credit of the many private companies in the field.
But there is no recent verification tool that has been enabled by any new core technology. Nothing wrong with this, it is partially the consequence of a mature industry, where most of the effort goes into improving the customer experience and helping him integrating verification and design/synthesis flow.
When Randy Bryant published his BDD paper in 1986, he revolutionized the field of formal verification with a technology that could address problems previously out of reach. When EC switched from BDD to SAT solvers nearly 10 years ago, it made possible verifying multi-million gate designs against their RTL description. Bounded model checking became a practical approach to sequential property verification. These were disruptive technologies. Where is the next leap?
From the business point of view, force is to admit that the formal verification market has been pretty stable. Most of the ever-increasing design cost is taken by verification, but that does not translate into a fast growing formal verification market. Instead, the more and more daunting verification task benefits simulators more than formal tools. Yes, customers are slow to move to a different verification flow. Yes, the formal verification industry, as the rest of EDA, struggles to find a business model that would bring back a much needed growth. But which application or technology will bring enough value to make the ratio simulation/formal in favor of the later?
Regarding the simulation vs. formal debate, I would recommend reading Chris Wilson’s comment. He agrees with me that formal verification has had a relatively low return on investment. He then argues that simulators will remain the main verification solution, with formal verification technologies under the hood to speed up simulation, to increase coverage, and to help debugging. He may well have a point here.
One aspect that everybody agrees on is that debugging is still a bottleneck in the verification industry. Why does a design fail its functional requirement? Having a counter example (e.g., a sequence of inputs that disproves a safety property) is often not sufficient: the complexity and length of the counter example can make pinpointing the design error very difficult. A failing liveness property cannot be revealed with a finite sequence of inputs. Similarly, there is no tool that provides consistent debugging information explaining why a statement of a RTL description is unreachable. Formal verification techniques can certainly help here, and there are a few available products aiming at the problem.
In conclusion, formal verification as an industry has matured, but is still looking for the market share it deserves. I think there are a lot of opportunities to grow the market. Success may come as an enabler of a better, faster, high coverage, simulation. I rather believe it will come when formal verification allows software and hardware to be verified and debugged in a common, continuous, design flow. And this requires some major technical innovation.