regarding your points on why some companies do not adopt
high price of tools, Here you need to consider ROI - can a single proof replace days of simulation?
how easy to use in complex design or SoC good point - I think we will still need experts but the apps will get more sophisticated allowing the basic user to do more sophisticated proofs. I think small companies (such asTVS) could write "assertion generator" apps for some sophisticated scanrios
and simulation time with formal Another good point but I think it is more the unpredictability of formal run times that is more the issue
We haven't got all the answers yet but we're moving in the right direction
Mike, interesting article and discussions. I agree formal apps will help drive formal adoption in the industry, so is End-to-End formal, or "full expert formal". However "full expert formal", despite the hurdles you mentioned (e.g. writting checkers, overcoming complexity etc), does not require formal experts. I have just published a blog on our website yesterday on this topic "Formal Verification, by Everyone and for Everyone". Oski CEO Vigyan will be giving a talk at the upcoming Austin SNUG on the same topic. As a dedicated formal services provider, we are working very hard on promoting formal adopting in the industry by using formal for sign-off.
Thanks Mike to give us a comprehensive view of formal verification and tools' use model.
Formal Apps had helped people to find many buys in different scenarios(especially in unreachable code coverage analysis, CDC, Connectivity, X-Propagation), I believe Formal should be the mainstream in near future regarding its powerful capibilities.
However, some companies didn't adopt it, the reason may be the high price of tools, how easy to use in complex design or SoC and simulation time with formal.
Nice article - very interesting - especially since it covers formal apps from multiple vendors. My experience is that once engineers start to see the power of formal, the issues it uncovers that aren't uncovered by other techniques, they're keen to delve a little deeper. And of course these apps add value in themelves - even though we apply a full, complete formal verification on units, we'll still use the apps at higher levels of hierarchy.
From what I have seen of different customer adoption models, apps can be a way to use formal technology but, as Darren G commented, until people are writing properties and verifying them they aren't really using "formal".
However, once users find the trapdoor in the belly of the horse (and that trapdoor can be a bit sticky) there's usually a lightbulb moment. Designers, in particular, can find that they suddenly have access to a lot of verification horsepower.
Coming at this from the perspective of working at three different EDA vendors in this space, I completely agree with the crux of this article. I've seen first-hand how formal apps can indirectly grow the usage of formal in customers/verification domains that had previously shunned classic formal analysis. Why? In a nutshell, the fact that formal apps are structured in terms of the customers' problems (and not the other way around, as is often the case with other EDA tools) is IMHO the primary success factor here. Of course, the exhaustive nature of the formal engines under-the-hood of the apps' customized GUIs and supporting automation is a huge plus that customers appreciate. Finally, it's important not over-hype the maturity of the apps model today by noting that most formal apps aren't perfectly plug-and-play. That said, depending on the circumstances quite often a half-day of coaching from an AE is enough to get the user up and running.
I agree that "full formal" will still require "full formal experts" which will limit how far it can be deployed. But, as pointed out by Graham, I wonder if the scope of "apps" will increase to take in areas which we currently consider as "full formal"? I think the AXI interface is a good example
This coud be a very good business opportunity for smaller companies to produce a suite of assertions for specific applications (or more likely an app to generate them) that can be used with all of the tools for the bigger industry players?
NASA's Orion Flight Software Production Systems Manager Darrel G. Raines joins Planet Analog Editor Steve Taranovich and Embedded.com Editor Max Maxfield to talk about embedded flight software used in Orion Spacecraft, part of NASA's Mars mission. Live radio show and live chat. Get your questions ready.
Brought to you by