Verification Guild: Ottawa Chapter: Meeting #1 - Minutes

bryan_morris_peng · Senior Joined: Jan 08, 2004 Posts: 10 Location: Ottawa

===============================================
Meeting Minutes for Verification Guild: Ottawa Chapter - Meeting #1
===============================================

Date: December 2nd, 2004
Time: 7:30PM until 9:30PM
Place: Brookstreet Hotel.(525 Legget Dr)

Presenters: Dan Benua, Synopsys, CAE Manager, Verification Technology Group &
Bryan Morris, S2io ASIC Verification Team Leader and Whipping Boy.

Approximately 35 people showed up for the first meeting of the Verification
Guild of the Ottawa Chapter. Bryan Morris welcomed everyone and put forward his
ulterior motives for starting a chapter (share best practices; stop re-inventing
the wheel and a fun networking event); what kinds of things we could and should
do with the chapter; laid out some of the ground rules for how to be on your
best behaviour at each chapter meeting. Bryan then proceeded to break his own
rule by dissing RTL designers in a cavalier manner. Smile

I guess I'll be getting
a lump of coal this year.

Many thanks went out to Janick Bergeron for his help in getting a guy like Dan
Benua (see next paragraph) to come and give a presentation. Thanks also go to
James Aitken, Synopsys Account Manager for his help in setting up, and most
importantly, paying for the room at the Brookstreet Hotel.

Onto the "meat" of the event: Dan Benua a Formal Verification Guru from Synopsys
gave an excellent presentation on the theory of how Formal Verification works.
Dan went on to explain some of the benefits and issues in adopting an Assertion
Based Verification (ABV) strategy and a formal tool into a verification flow.

What follows is my interpretation of what Dan talked about in his presentation
and I've added my own thoughts. It likely combines breathtaking brilliance and
insight, mixed with some unbelievable ignorance about what Dan *actually* said.
As always, it's open for discussion...

Key Benefits of ABV

* assertions concisely describe temporal behaviour;
* debugging assertion failures points directly to the origin of the issue;

Benefits of a Formal Tool

Once you have assertions in your flow, a formal tool can:

* check for design compliance without a testbench -- the assertions should
define the expected behaviour;
* the promise of finding corner case bugs that would be difficult to find in
a testbench (with directed or constrained random testing);
* *could* exhaustively prove a circuit under all conditions (which, for some
cases is *impossible* with dynamic simulation because of the number of
possible conditions that could be applied).

Key Challenges of Adding a Formal Tool into your Flow

Assertion Languages: You gotta learn a new language and debug flow. SVA
is a declarative rather than imperative language which is a different
model for many H/W designers/verifiers.
Formal Capacity: The capacity of tools is easily impacted by the design
size; number of assertions present; cone of logic entering into an assertion
point and others. This can be handled by the designers partitioning the
assertion design such that it attacks "smaller" chunks (i.e., smaller
design size, less assertions, smaller cones of logic, or any
combination). Hybrid tools allow the formal tool to be kicked off from the
dynamic simulation point of interest, which can reduce the set of initial
states the formal tool can start from.
Constraints: Constraints are added to a formal tool to ensure that you're
eliminating any initial conditions or impossible states (e.g., you have
three modes specified in a byte field -- you can probably eliminate the
other 253 possible starting states for that mode value. Need to hit a balance
between under-constraining the solver resulting in extra debugging effort;
and over-constraining the solver that could create a false proof (i.e., the
solver says it's OK, but it's not).
Completeness: How do you know when you're done? The end result is that you
must rely on experience that will grow with time. A handy feature: You can
use the tool to generate reports on which areas of the design have not been
covered. This should guide you to add or change existing assertions, or
use the testbench for covering those areas.

Reducing the Adoption Barrier for ABV and Formal

Learning Curve:

* Use the set of pre-built assertion libraries (e.g., most if not all
vendors have a library of assertions to handle common checks (e.g.,
underflow, overflow, one-hot, etc.). You can use these libraries as
building blocks for your custom assertions;
* Use the assertions in simulation to assist in the debug cycle;
* Develop custom assertions for the blocks you intend to formally prove;
* Add the constraints to the formal tool incrementally;

Scaling to Higher Levels of Abstraction:

* assertions are great for pin-level checks -- don't expect them to scale
to a transaction level;
Note from the moderator: this point has spawn this topic.
* don't expect them to replace HVLs anytime soon for system level
checking;

Scaling to Large Numbers of Assertions:

* group assertions by functionality that they check (e.g., checking
handshaking), or structurally on types of circuits (e.g., checking FIFO
proper behaviour);
* group assertions separately for simulation and formal;
* after the easy assertions are verified disable them or add them as
constraints to reduce the amount of work the solver must do on each
pass;
* carefully prove each "hard" assertion one-by-one. The "term" hard is
defined at your discretion;
* include only the constraints that are necessary and relevant for the
problem to prove.

Other Good Tips:

* set reasonable expectations on when you'll become proficient in
assertions.

<Bryan's opinion>

It *likely* **won't** be the first ASIC
you use them on; it *may* be the second ASIC you use them on; it *likely*
will be the third time that you use them to their fullest potential

</Bryan's opinion>

* formal has it's place; dynamic simulation has it's place -- they are
very complimentary to each other **and** attack the problem from two
different domains which is always a good thing.
* work with your EDA vendor. They are an excellent source of methodology
and they may have worked through some issues you may be struggling with
either internally, or with another customer.

Dan did an fantastic job in outlining the formal verification space without
being too Synopsys-centric. It was appreciated by everyone who attended.
There's only word for the presentation: EXCELLENT. Thanks, again to Dan and
the Ottawa Synopsys team.

Next Meeting?

Bryan outlined some ideas for what kind of topics are of interest (to me at
least) for future meetings including, but not limited to the following:

1. User experiences with formal verification tools;
2. SystemVerilog : Current state of affairs (tools, language, etc);
3. Assertion Based Verification: (PSL, SVA, others): User Experiences and Opinionsl
4. Reuse Verification Methodology (RVM): User experiences;
5. SystemVerilog Verification Library : A brain child (or brain fart) of Bryan's to create an open source library of useful base utility classes. Janick suggested using his Verification Methodology Manual as a starting point. Excellent idea

After the event closed off, I had three people volunteer to do presentations on
#2: SystemVerilog current state; #4: RVM User Experiences; and a discussion of a
Verilog-based library of useful utility tasks and functions.

I'll post the list of possible presentations shortly before the next event for
discussion. Or I may just act like a *benign* dictator and choose one. In the
interim, please feel free to ping other ideas off me in this forum, or
privately.

Apres-Meeting Socializing

Then I drank a beer with a smaller group of stalwart individuals, put on my
touque and went home to sleep. Oops! Maybe *too* much information.

Chapter Appreciation Section

All in all I think we're off to an excellent start! Thanks to everyone for
attending. You *exceeded* my expectations for this event.

And you're welcome. It was my pleasure. Smile

Next Meeting
:Date: Tentatively Scheduled for Monday, March 8th, 2005...
:Place: Somewhere in Kanata...tbd Ideas on a cheap/free place to run this
from would be most appreciated.

Merry Christmas, Happy Chanukah, Season's Greetings, Happy Kwanzaa, and of
course, Happy Festivus to Seinfeld fans everywhere.

Happy New Year. Enjoy the snow -- it's *only* going to be here for another 5
months and then back to hot and sticky summer

Bryan