( ESNUG 563 Item 9 ) -------------------------------------------- [03/09/17]
Subject: Raik and Hogan on formal apps, formal engines, and SNPS VC Formal
DAC'16 Troublemakers Panel in Austin, TX
Cooley: Raik.
Raik: I'm still here.
Cooley: Every formal vendor out there is saying, "We got apps, we got
apps, we do apps." Isn't that just candy-coating a real
pain-in-the-ass problem of formal verification?
Wait a minute, do you, One-Spin, have apps?
Sawicki: Don't knock candy coating.
Raik: Does One-Spin have apps? Doesn't everyone have apps? I mean,
yeah, sure. Everyone has apps, and they are there for a very
good reason. It's not actually hard to apply formal but it's
actually hard to use formal effectively for specific problems.
What apps are doing is they encapsulate recurring verification
tasks into some form where you can easily use them and make
them more productive, more reliable, and more scalable for your
team. So that's what apps are doing.
The virtue is really that you still need to learn how to use
the apps but you don't need to understand exactly how to work
a particular problem.
Cooley: My understanding is that Vigyan from Oski is making a ton of
money doing consulting just on how to run formal.
Raik: Yeah, he's making a lot it out of it. I think the thing with
formal is that beyond apps you also need to verify
functionality. That's not done by apps, that's done by
writing assertions. Assertions haven't been the problem, as
such. The problem has been... One "for example". You can
write assertions. You can teach it in 4 days or something to
people and make them productive at writing assertions. It's
much easier than UVM. But the real problem was that people
didn't know what they meant, if they've got to prove them.
So if you get failures, that's fine, you can debug them, that's
great. So if you get a trace, you get a short trace, even with
formal, that's also pretty beneficial.
But what if it's proven? You've got an assertion that's done,
and then what's next? How do you know what you have actually
achieved? That's where coverage comes in, as I mentioned
earlier. You need a precise coverage metrics for formal, and
that's what we pioneered.
Another problem that people ran into was the engines. You can
have 8 engines, 18 engines or how many engines. It's a PhD
tool. You can have 100's of switches for each of the engines
and that's not really something that people would like to know
or would like to do.
There are some PhD's who will invent a 19th engine for you and
you'll come up with creative ways of writing scripts and
combining them. But what you really need to make formal
scalable is an architecture, and a tool that can select them
automatically, set the parameters automatically, so you don't
have to fiddle with them.
Some companies make an art of formal, but if you have right tool
you should just be able to push a button; that's where we at
One-Spin have been working a lot on creating a better an
out-of-the-box experience with formal. So you really don't want
people to mess around with the proof engines.
Cooley: What do you think about Questa 0-In? Jim just did a giant white
paper on all sorts of formal tools and one of the things that
stood out was 0-In Questa stuff was very weak, along with
Synopsys VC Formal... (See ESNUG 558 #5)
Hogan: [looking at Raik] Cooley's misquoting me usually, so keep going,
keep going... Ok, ask your question, sorry.
Cooley: Ok, I'll be very specific. What have you heard about Aart's
Synopsys VC Formal?
Hogan: I haven't heard of Synopsys VC Formal, to be honest with you.
No customers have come up to me and talk about it. And I ask,
right? So what do I think? I think exactly what Raik said:
It takes a while to mature these things. Like place and route
takes a while to mature.
And there isn't one formal engine for everything. There's a
bunch of formal engines, and it takes a while to build those
formal engines and then tune them to the specific problems.
So that's the challenge for Synopsys in my opinion.
Cooley: Raik, Synopsys VC Formal?
Raik: I haven't seen them. I heard that Synopsys is working on
something, and it probably will take some time to make it
work. As I said, it's not that easy, and we haven't seen
them out there. I suppose they don't want to make a mistake
in announcing something big and then have a big failure;
we have seen that before.
Cooley: IC Compiler, IC Compiler II... [audience laughs]
Raik: Aart doesn't want to run into that issue, especially with
formal which is a key technology. So you want to be sure
it's working.
In the meantime we at One-Spin are doing, based on the working
platform, new things that they won't go after.
That's things like opening our platform to 3rd parties like
our customers to write apps. We don't write all the apps
ourselves, it's the customers who are doing the apps.
Cooley: Oh that's right. You're doing that platform thing.
Raik: There are companies like Tortuga Logic specializing in
security. There's a company like Agnisys doing
specification-to-implementation with formal verification
based on our platform, which is open in that sense, that
they can license it. Our customers, as I said, write their
own apps.
The flexibility and scalability of the platform that makes
a difference in the end. If you want to go broad with formal;
if you really want to have the third leg in your verification
flow based on it.
Cooley: Ok.
---- ---- ---- ---- ---- ---- ----
Related Articles
Anirudh and Sawicki on IC Compiler II, Innovus, Nitro-SoC, Antun
Amit and Sawicki on Cadence Spectre, Synopsys HSPICE, Mentor BDA
Dean and Sawicki on Big Data tapeout predictors, John Lee's Gear
Raik and Hogan on formal apps, formal engines, and SNPS VC Formal
Anirudh and Sawicki on iffy Apache IR-drop #'s vs. Voltus/Innovus
Join
Index
Next->Item
|
|
