Saturday, November 16, 2013

Formal users share 8 upsides, 6 downsides, and 13 best practices, thanks to Vigyan Singhal, real formal users, and John Cooley

Nice summary article by Vigyan, thanks to John Cooley's DeepChip:

( 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:


   "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."

          ----    ----    ----    ----    ----    ----   ----
          ----    ----    ----    ----    ----    ----   ----
          ----    ----    ----    ----    ----    ----   ----


   "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."

          ----    ----    ----    ----    ----    ----   ----
          ----    ----    ----    ----    ----    ----   ----
          ----    ----    ----    ----    ----    ----   ----


   "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

    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

    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, CA
Formal users share 8 upsides, 6 downsides, and 13 best practices

'via Blog this'

No comments:

Post a Comment