Will Formal Really Dominate Verification?

Today’s post is prompted by a recent article on SemiWiki in which Jasper Design Automation’s CEO Kathryn Kranen is quoted as saying “formal will dominate verification.” There is a nice set of metrics from Jasper’s recent User Group meeting showing their impressive growth in revenue, logos, users, and licenses as supporting evidence for formal’s increasing footprint. The article concludes by stating “at some point in the future, formal will be the default choice for every verification task in the way that simulation/emulation is today.”

That made me sit up and take notice. Before joining Breker, I spent the previous 12 years of my career focusing on formal analysis, about six years full-time and the rest as one component of a wider suite of verification products I managed. I’m a big fan of formal, but I don’t think that I can comfortably predict that it will “dominate” verification. Let  me share my thoughts.

I have no argument whatsoever that formal has proven highly valuable on many types of designs at the block or subsystem level. If you can specify your intended behavior in the form of assertions and your design isn’t too big, formal can be very effective at verifying 100%. Simulation of course can never approach this bar, hence the interest in formal. Jasper has done a good job of convincing IP teams that formal must be part of their verification arsenal.

At the full-SoC level, formal is overwhelmed. The sheer number and depth of paths to be analyzed mean that 100% proof of all assertions is unlikely. However, there are many specific applications for formal analysis running at the full-chip level that do not need to analyze the entire design. Examples include verification of I/O port connectivity, clock-domain crossings, and power-domain control. Jasper has done an excellent job of packaging and delivering these “apps” to mainstream users.

However, I am really dubious that formal can replace simulation and emulation for “every verification task.” In addition to the the capacity issues, some protocol generators and checkers are hard to express in terms of assertions alone. Especially for deep serial protocols, the assertions must be supported by a lot of RTL “helper” code, all of which must be formally analyzed with even more stress on capacity. Some behaviors are easier to express and check in simulation than in formal.

Dynamic power analysis, in which switching activity is measured for long emulation runs, has no formal equivalent. If possible, these measurements are made while the chip is running production software, typically an operating system and end-user applications. It is essential that the hardware and software be co-verified, most likely in an emulator or FPGA prototype rather than in slow RTL simulation. Formal offers no help or replacement for this portion of the verification effort.

So I have to respectfully disagree with Ms. Kranen’s bold statement. But mulling over this topic led me to the related question of whether Breker’s graph-based approach will ever “dominate verification.” I have some thoughts on that topic that I’ll save for my next blog post.

Tom A.

The truth is out there … sometimes it’s in a blog.

Tags: analysis, Breker, emulation, formal, FPGA, functional verification, graph, IP, jasper, Kranen, scenario model, simulation, SoC verification, test generation, TrekSoC, TrekSoC-Si

This entry was posted on Wednesday, November 13th, 2013 at 3:27 pm. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.