( ESNUG 534 Item 5 ) -------------------------------------------- [11/15/13]
From: [ Vigyan Singhal of Oski Tech ]
Subject: Formal users share 8 upsides, 6 downsides, and 13 best practices
Hi, John,
My company, Oski Tech, hosted our first "Decoding Formal Club" on Oct 10 in
the Computer History Museum in Mountain View. It was a small invite-only
event for verification experts to discuss their general in-the-trenches
"ups" and "downs" of using formal tools. (Oski is a consulting house for
formal tools. We advocate using formal -- but not any specific brand or
make of formal tools. Over the years we've used JasperGold, Cadence IEV,
Questa Formal, OneSpin 360 DV, Synopsys Magellan.)
We had 15 formal users from 10 companies -- Apple, Broadcom, Cisco, Nvidia,
HiSilicon, Memoir Systems, Microsoft, Palo Alto Networks, Qualcomm and a
stealth start-up attended the event. To present a fair view, only half of
the companies there were Oski customers.
After our presentation on "Using Bounded Proofs for Formal Sign-off", we
asked these formal users for their bittersweet moments of formal tools.
Here's what they said:
THE UPSIDE OF USING FORMAL TOOLS:
"I have been working on formal verification for about a year, working
with two designers. The first person designed the parser for our
switch. He was shocked to see real legal packets showing in the
waveform on the first day of running formal with little setup and
constraints. We had a lot of good luck verifying the parser with
formal and found a lot of bugs that the regression was missing.
Also this design was based off a previous design that was already
taped out and the chip was being sold. So formal was a good tool."
---- ---- ---- ---- ---- ---- ----
"I have started doing model checking on IPs and we've found 2 or 3
complex bugs that designers think are difficult to find because
you have to send many packets to reach those full conditions and
exercise those. Formal was really helpful."
---- ---- ---- ---- ---- ---- ----
"We are using formal in my project to solve real problems. Whenever
there are specific issues where we think formal can help, for example,
clock gating in legacy modules, anything we didn't feel comfortable
that simulation could do a good job verifying, we won't let it go
until we get full proof using SEC.
Another scenario where formal is very successful is post-silicon
debugging. By knowing the design and using formal we could get good
closure in solving the issues seen in the lab.
Clearly you all need to know the design inside out. Because you need
to make an educated guess as to what the proof might be and try to
hit the state using formal. We have been very successful. It is
hard and lots of luck as well!"
---- ---- ---- ---- ---- ---- ----
"I see value in formal because designers asked me to help with corner
cases that are hard to find in simulation, most of the time I was
able to find the bug. That was very fulfilling."
---- ---- ---- ---- ---- ---- ----
"I am finding clock/reset issues by using formal that would be show
stoppers not findable in simulation."
---- ---- ---- ---- ---- ---- ----
"We make IP. Our customers won't buy our IP without us using formal;
so formal is a requirement for us. We don't have the luxury of test
chip so everything we do has to be full proofs, not even bounded
proofs. I have been doing formal for 3 years but I have a lot of
design and verification experiences.
What's interesting is I use formal to help me design faster. I use
it when I am writing code and formal helps me debug and I am done
a lot faster."
---- ---- ---- ---- ---- ---- ----
"We were worried about deadlock in our ring environment. There are
two ways of using formal. One is finding bug, which everyone
agrees is good; another is achieving closure. We are still a bit
nervous about using formal only for sign-off. My management thinks
we need to get stronger with formal and to include formal sign-off
in addition to simulation."
---- ---- ---- ---- ---- ---- ----
"Formal gives me more flexibility and confidence to rewrite my code
than I would have because it gives me safety net. You do a lot of
patches because you are worried about breaking something. But you
can rewrite more freely if there is a tool that could catch you."
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
THE DOWNSIDE OF USING FORMAL TOOLS:
"Our problem with formal is to debug over-constraint. We have 800
constraints. It's impossible to go over each constraint one by one.
The formal tool we have lets us narrow down constraints. However,
for over-constraint caused by multiple constraints, it is still hard."
---- ---- ---- ---- ---- ---- ----
"I don't like that I need to write constraints for black-boxed module
when using formal. For example, big register banks, which I must
black-box to reduce compile time, but then I have to write lots of
constraints that this flop will be the same in one cycle and next.
Also there is effort for memory modeling, because most memories have
behavioral code which formal tools can't handle.
There is no general way of reuse much of it."
---- ---- ---- ---- ---- ---- ----
"We struggle on how to communicate how formal works versus simulation
to other engineers. Progress in formal is different than progress
in simulation and is hard to communicate."
---- ---- ---- ---- ---- ---- ----
"We can't integrate coverage from formal into simulation. When I am
evaluating coverage, I don't have the spare time to spend on blocks
that I have already spent with formal."
---- ---- ---- ---- ---- ---- ----
"Our problem is when maintaining regressions with 100s of properties,
any small design change break many properties. These design changes
are less an issue for simulation guys because they run at higher
(chip) level using transactors.
Should formal fit in the verification methodology like simulation?
It is hard to feel valued, as formal regression doesn't find many
bugs, which is typically what people judge formal success by.
Formal sign-off rather than bug hunting should be the goal of formal."
---- ---- ---- ---- ---- ---- ----
"The biggest headache I see in formal is getting the spec. At module-
level often there is no spec. Sometimes the designer is busy and
doesn't understand why you want to know the interface.
It's a struggle. You have similar problems in simulation but it's
even more of a problem for formal."
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
FORMAL BEST PRACTICES:
"I think it is much better if designers - while they are designing
small modules that they start off using formal, because they are
better able to write constraints for the environment."
---- ---- ---- ---- ---- ---- ----
"I would like to have my design verified by formal as much as
possible. A simple bug can blow up to big issue if found later
on. It's better to run formal on block level early.
For example, designers can check IO protocols in formal before
passing the design to integration."
---- ---- ---- ---- ---- ---- ----
"Re-use properties. We started a flow to go through the design,
through the interfaces, and see if there are properties you
could pick up and use. That way as a designer, they are not
spending any time to write properties that are already there."
---- ---- ---- ---- ---- ---- ----
"We are also building formal flow for our designers to write their
assertions for smaller blocks."
---- ---- ---- ---- ---- ---- ----
"We are not gung ho on full proof -- we use it only to shorten
schedules and manage risk. We cherry-pick our projects. We
interview people and ask designers and management about their
worries. If there were coverage issues in simulation or their
design is changing, it would be good formal candidate."
---- ---- ---- ---- ---- ---- ----
"We have a surgical approach in formal verification. When we were
laying out the test plan for our blocks, we identify things that
are hard to achieve in functional simulation and verify those
with formal.
For example, statistic blocks with aging functionality and a whole
bunch of instructions.
When I was building up our UVM test bench, I incorporated formal
checkers into simulation. This helped a lot because while I was
churning out test cases, the formal checkers would fail and that
helped me debug much quicker.
Even though I am only halfway through, I am already see a payoff
using checkers written for formal in simulation."
---- ---- ---- ---- ---- ---- ----
"I found formal to be effective when I work on properties where the
designers/verification has coverage concerns. I can find corner
case bugs quickly with formal."
---- ---- ---- ---- ---- ---- ----
"I have been doing complete verification using simulation since 1989.
I think you need to apply formal on places where simulation has
weaknesses.
We look at the design, if we can write exhaustive test, we don't
bother with formal.
When there is no way to hit all corner cases, situations that will
take simulation years and years, then we are going in with formal.
You have to be bug-focused, to find show stoppers, formal can go
through it, and be done with it once for all."
---- ---- ---- ---- ---- ---- ----
"The large portion of the community that uses formal uses it from a
verification point of view, which I think is reactive, more of an
after-thought.
If I had to go and construct a team to build the chip right now, I
would actually completely rearrange how the whole build would be.
It would start with designing using formal. Adoption for formal is
a lot more powerful if you come at it from a design background."
---- ---- ---- ---- ---- ---- ----
"We are designing memory, so everything is parameterized. If we
can't get a proof, we just change the size of the design and get a
proof from that.
That's a lot of power for formal as you can change the parameters
but still get full proof on the whole design."
---- ---- ---- ---- ---- ---- ----
"We are part of our group's design team, so there is no blame game,
easier for us to get a spec and get acknowledged when we find bugs."
---- ---- ---- ---- ---- ---- ----
"We make progress in formal by building good relationship with our
designers -- they understand that if they give us a little bit of
time to explain what the design is supposed to do, then we can
give them back a very high quality design."
---- ---- ---- ---- ---- ---- ----
"It would be good to have "formal friendly" design specification, as
sometimes the bugs are results of interaction of 7 or 8 designers.
People sometimes have misunderstandings of what a specific paragraph
in a document means."
---- ---- ---- ---- ---- ---- ----
I want to thank the participants for sharing their thoughts and real-life
stories on using formal tools.
- Vigyan Singhal
Oski Technology Mountain View, CAFormal users share 8 upsides, 6 downsides, and 13 best practices'via Blog this'
No comments:
Post a Comment