( ESNUG 544 Item 2 ) -------------------------------------------- [11/14/14]
From: [ Normando Montecillo of Broadcom ]
Subject: How I unwittingly started BRCM's Formal Verification Users Group
Hi, John,
I belong to the set-top box group in Broadcom doing video display engines.
Like every other group inside of Broadcom, 5 years ago we were doing SW
simulation and HW emulation as our only form of verification.
For top-level verification, we spent more and more of our time chasing
failures. In the last 2 years, our debug time doubled as we found that
datapath problems could easily take 2 days each to debug -- as the number
of tests we ran increased by 4X.
We looked around and came to the conclusion that System Verilog Assertions
(SVA) might help. We chose SVA over Property Specification Language (PSL)
assertions based on the rate of adoption we are seeing in other companies;
plus what's reported by the media. I was given the task of looking into
assertions and see how we can take advantage of them.
There was no vision of a bigger road map -- only a simple desire to keep
improving. Some attempts worked and others did not.
OUR FIRST TEMPLATES
We set up a small, two-person taskforce to write assertions part-time,
learning the syntax, writing checks, and running simulations to verify
their correctness.
We found out quickly that transforming our intent into an assertion is not
easy, and debugging assertions can become time consuming using simulation.
We needed to write better assertions, and we would need to allocate time
for our verification engineers to develop their assertion writing skills.
I was fortunate that management agreed that this was a good investment.
With two engineers and with some practice, we were able to create a set
template assertions for the rest to follow.
THEN THE DESIGN ENGINEERS
The next hurdle was selling assertions to our design engineers. The design
engineers' responsibilities were growing as they were being asked to do
more and more -- so they were not receptive to added responsibilities.
Making it mandatory is the only way to get them to move forward.
On our first project involving assertions, we mandated that every design
engineer had to write a minimum of 10 assertions. We set the bar low
enough so that we could guarantee success.
Yes, they each met their target of 10 assertions each, but they weren't
very good at first. A lot of the assertions were done just to make the
mandated number of assertions.
But two design engineers who attempted to write meaningful assertions had
found some success. With that success, more of the design engineers were
motivated to write more assertions. And then they continued to write more
assertions on subsequent projects. Their successes in turn converted a
few more design engineers towards Assertions Based Verification (ABV).
SLOW FULL FORMAL BUY-IN
With our assertion pilot program slowly gaining momentum, we were looking
for the next step in improving our verification methodology.
At this time, we had a design module that we were struggling to get good
coverage on. It was an arbiter with 32 clients and dynamically changing
priorities and masking that was a code coverage nightmare.
With the help of a Cadence AE, we formally verified this arbiter using their
IEV tool, extracted coverage, and merged them with our Verilog simulation
coverage numbers to hit our target coverage goal. The presence of that AE
was critical at that time. His conviction and success has led us to explore
formal formation. We fell into the formal verification path. It wasn't
planned, it just happened.
BUT I'M A SIMULATOR JOCKEY!
At the time, my primary job was to do design verification using standard
commercially available Verlilog simulators like VCS, Incisive, and Questa.
Pursuing formal was not officially given to me. It was something that
interested me and I had the strong desire to pursue. I lobbied for time
to pursue formal and was happy that I was given some time, but at a lower
priority. My simulation tasks took precedence.
Sometimes, I had to use my own personal time to explore ABV with the
Cadence IEV tool and I had to deal with the usual struggles of learning
something new. Getting over the ABV learning curve took some time.
I learned to navigate this formal tool, writing effective constraints,
capturing the problem with good checkers, and debugging counter-examples
provided by IEV.
CADENCE IEV VS. JASPER JASPERGOLD
Then we made the switch from the Cadence IEV formal verification tool to
the Jasper JasperGold (this was before the acquisition) as we saw some
advantage in debug analysis with JasperGold instead of IEV.
Jasper Visualize (click pic to enlarge)
What I liked about the waveform debugger, Jasper Visualize, is that you
can manipulate the waveform to expore your design. It can generate
on-the-fly covers, change signal values on any clock, and then generate
a new trace. Once that trace is displayed, you still have traditional
waveform debug features -- like tracing the source of a value change.
  
Luckily, I had the help of a Jasper AE for the JasperGold tips -- plus the
help of Vigyan Singhal from Oski Technology -- who was instrumental to my
formal skill improvements. Vigyan and I had a lot of discussions on
verification strategies through email, text messages and lunches.
I DRANK THE KOOLAID
I finally got to a point where I was finding real bugs. The more bugs I
found, the more I wanted to find the next bug. I was starting to see and
understand a verification approach that is different from simulation -- one
that requires a different mindset, and one where my simulation experience
was sometimes hindering my formal development.
"Our Verification Flow BEFORE Formal" (click pic to enlarge)
I made a decision that formal is something I wanted to do full time so I
lobbied to change my responsibilities. It didn't happen right away, but
eventually I was able to convince my management to make me full time on
formal. It finally happened January 2013 when I was officially a full-time
formal verification engineer at Broadcom. My perseverance, my motivation
and my passion for formal convinced my management.
My first task was to grow formal verification use in my group. This is when
I started the Formal User's Group inside Broadcom -- with regular one hour
meetings where I could discuss "formal" topics. I used this meeting to
promote formal success stories, not only from myself, but others as well;
to share techniques that worked, and to invite outside speakers to talk.
This was important, as success breeds more success, but I needed to clearly
demonstrate it. I started out with one small internal users group meeting
and today we now have all formal users inside Broadcom in our email list.
MAKING FORMAL EASY
Aside from promoting formal, I wanted to make it easier for the Broadcom
engineers to get started using formal, so I created/improved scripts for
tool setup, design configuration management, formal-friendly libraries,
and creation of standard driver/constraints library.
"Our Verification Flow AFTER Formal" (click pic to enlarge)
I also worked on standardizing flows, including reverse connectivity (a
common formal task) and creating a standard TCL script as a starting
point for groups wanting to do reverse connectivity.
Lastly, I make time to work with groups that are just getting started. I
help by picking formal-friendly designs, checker constructions, constraint
generation, debug, and simple abstraction.
I believe if no one person does not "own" all of this, formal gets adopted
rather haphazardly inside your company.
In parallel, I am also grow my skills by working on select designs and
applying formal verification techniques to them. Throughout this, Vigyan
and the Oski consultants provided valuable support whenever I got in over
my head. Having veterans to help when you're stuck is crucial!
NORMANDO'S ADOPTING FORMAL TIPS
The advice I would give to any company looking to adopt formal are:
1. Make sure you have a champion in the company who is enthusiastic
about formal verification to charter the effort;
2. Make sure you have formal experts to support you in the effort
because formal is VERY different from simulation. It takes time
and effort to develop practical formal verification skills.
Access to formal experts can save a lot of time, effort, and pain;
3. Make sure formal is a full-time job for your formal champion.
Formal is orthogonal to simulation and requires a different
mindset. You can't easily switch from one realm to another.
4. Make sure you set realistic expectations and goals at the beginning
and keep improving one step at a time. There is no way around it.
Improving formal skills requires practice and experience.
And, again, it pays to have formal experts to show you the way.
Looking back, I'm proud of what we have done at Broadcom in the last 2 years
for formal verification adoption. After all, who wants to lose sleep at
night wondering if there are still bugs lurking in your chip? For that,
nothing beats formal.
- Normando Montecillo
Broadcom Corp. Santa Clara, CA
Editor's Note: For 11 years, Normando designed video and audio cores
at Broadcom DVT, then for the last 5 years did verification for that
same group, first on simulation, then accidentally on formal. - John
---- ---- ---- ---- ---- ---- ----
Related Articles
Formal users share 8 upsides, 6 downsides, and 13 best practices
Mark Wallace of Cavium's Jasper User Group (JUG'13) Trip Report
Jasper SEC & Datapath versus Atrenta BugScope were #2 at DAC'13
Join
Index
Next->Item
|
|
