Breaking News
Blog

Are Formal Apps a Trojan Horse?

View Comments: Newest First | Oldest First | Threaded View
Page 1 / 2   >   >>
roman.wang
User Rank
Rookie
Good Article
roman.wang   9/14/2014 10:51:11 AM
NO RATINGS
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.

Effort to implement may be another concerns. 

 

 

 

anon4939819
User Rank
Rookie
Nice to see mutilple formal tools mentioned
anon4939819   9/12/2014 2:54:54 PM
NO RATINGS
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.

Lampshuk
User Rank
Rookie
Up to a point
Lampshuk   9/11/2014 6:27:08 PM
NO RATINGS
(ex - Jasper employee, now at Cadence)

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.

And that's enough mixed metaphors for one post.

MikeBartley
User Rank
Freelancer
Re: Agreed!
MikeBartley   9/11/2014 4:33:50 PM
Hi Joe

I agree - most apps just require a short coaching to use. Our 2 day course ensures people are able to run the apps as well as apply a more general formal verification approach

Mike

jhupcey
User Rank
Rookie
Agreed!
jhupcey   9/11/2014 3:20:34 PM
NO RATINGS
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.

MikeBartley
User Rank
Freelancer
Re: Nice summary
MikeBartley   9/11/2014 12:39:17 PM
NO RATINGS
Glad to be of service 

Mike

Elephant Pete
User Rank
Rookie
Nice summary
Elephant Pete   9/11/2014 12:11:31 PM
NO RATINGS
Having been out of chip design for a few years I didn't actually know what a formal app was. Now I do!

MikeBartley
User Rank
Freelancer
Re: Formal Apps
MikeBartley   9/11/2014 5:23:13 AM
NO RATINGS
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?

Mike

Darren.Galpin
User Rank
Rookie
Formal Apps
Darren.Galpin   9/11/2014 4:46:14 AM
NO RATINGS
The point of Formal Apps is that they are using formal techniques to do their analysis, but they hide what they are implementing to achieve the result for the user. Thus someone who doesn't know how to use formal can use the tooling to achieve results. Hence I don't believe that this will really increase the use of "full formal" much, as that still needs the knowledge, but it will increase the use of formal engines within verification as a whole.

MikeBartley
User Rank
Freelancer
Re: Drivers for Formal Apps
MikeBartley   9/11/2014 3:55:53 AM
NO RATINGS
Thanks Graham

I especially like your your summary of the hurdles

(1) coming up with the assertions,

(2) controlling analysis complexity,

(3) debug, and

(4) absence of definitive outcome

And of course - apps help to solve all of these

Going forward - i agree that we need to find apps with a wider application. Wouldn't it be great to have a "verify my cache design" app!

Mike

Page 1 / 2   >   >>
Top Comments of the Week
August Cartoon Caption Winner!
August Cartoon Caption Winner!
"All the King's horses and all the KIng's men gave up on Humpty, so they handed the problem off to Engineering."
5 comments
Like Us on Facebook

Datasheets.com Parts Search

185 million searchable parts
(please enter a part number or hit search to begin)
EE Times on Twitter
EE Times Twitter Feed
Radio
LATEST ARCHIVED BROADCAST
David Patterson, known for his pioneering research that led to RAID, clusters and more, is part of a team at UC Berkeley that recently made its RISC-V processor architecture an open source hardware offering. We talk with Patterson and one of his colleagues behind the effort about the opportunities they see, what new kinds of designs they hope to enable and what it means for today’s commercial processor giants such as Intel, ARM and Imagination Technologies.
Flash Poll