( DAC 01 Item 17 ) --------------------------------------------- [ 7/31/01 ]
Subject: The Intel Case Study & Harry Foster's Assertion Checkers Hell
HARRY'S WARNING: On the technology level, this year DAC was the Year Of
The Assertion Checkers. There were boatloads of new and not-so-new
verification companies all singing the praises of designers writing
assertion checks in the source code of their chips. Even Intel presented
a much cited case study for the verification of its 1.5 million lines of
RTL code for its Pentium 4 and how they debugged it using 1 million
assertion checkers. Harry Foster of HP, at one of the DAC panels gave a
dire warning, though, about how each & every rinky dink little EDA company
is promoting its own proprietary set of assertions pecular to only that
company's product lines. It's going to be ugly, he warns. I agree.
"Intel Case Study
----------------
* The Pentium 4 has 1.5 M lines of RTL code.
* They quoted an industry average of approximately 1 bug for every
200 lines of code. Before silicon, Intel found 8000 bugs
(1 bug/187 lines), and after Silicon, they found another 100 bugs.
* They found 400 of the bugs via model checking, and 20 of the 400
would have never been found via simulation.
* Intel's compute farm ran 24/7 to give them 6 B cycles/week, but it
only amounted to less than 2 minutes of run time on a 1 GHz Pentium.
* He cited the following as key to their flow: verification plans,
directed random testing with coverage feedback to direct additional
testing, and 1 M assertion checkers.
I asked him about the designers' roles, and he said the designers only
did very basic testing with no real requirements. He said they ran
into problems near the "code turn-in" milestone because designers
started turning in untested code, creating too much burden for the
verification team. They had to turn the code back to the designers
to do basic testing even though it slipped a milestone."
- [ An Anon Engineer ]
"Harry Foster of HP, a participant on the Accellera/Intrinsix panel,
expressed concern that we were now going to have N different
assertion languages for N different tools. I fear that he is probably
correct. There were more assertion language related tools and
presentations than I ever anticipated. VERA had assertions. The
Verplex presentation talked about assertions and tying them into
formal verification. Verisity talked about assertions. Superlog
showed their assertions. Even Harry Foster gave a presentation about
the open OVL assertions available for free down-load at:
www.verificationlibrary.com. 0-in has assertions. And there was a
panel hosted by Accellera and Intrinsix on verification where much of
the discussion revolved about assertion languages.
I think there will be verification language wars for the next few years
until a few winners emerge. This is going to make the Verilog/VHDL
language wars look like a skirmish!"
- Cliff Cummings of Sunburst Designs
"Event Monitors and Assertion Checkers
-------------------------------------
This category aims to answer the question "Is the RTL functionally
correct?"
Harry Foster of Hewlett-Packard, co-author with Lionel Bening of
"Principles of Verifiable RTL", spoke at Verplex's demo suite.
Here are the key learnings from Harry's talk:
1. Create assertions on block boundaries during RTL code
development.
2. Focus on getting assertions into the code and not on the
technology for proving the assertions.
3. Start finding defects using these assertions.
4. Ask EDA vendors to support the Accellera assertion
language extensions.
Make support for the Accellera assertion language a requirement of tool
purchase. This enables users to develop confidence with assertions in
a known tool, such as a Verilog RTL simulation. This enables users to
leverage exactly the same assertion from simulation to other tools,
without being tied to a proprietary language.
Harry described a large ASIC where Hewlett-Packard found 85% of the
defects using Open Verification Library Assertions. They used the Open
Verification Library (OVL) to create 3000 assertions to verify a 10
million gate design. They found 85% of the bugs by OVL assertions.
OVL assertions added between the engineer's sub blocks create a
"verifiable contract". These OVL assertions check for illegal events
(state transitions, queue under and overflow conditions, one_hot
violation, et cetera). The OVL assertion violations are quickly
isolated during simulation. HP also puts OVL assertions inside
sub-blocks, but it's critical to have assertions between interfaces
of sub-blocks.
Interested in the Accellera assertion language? Check out
http://www.accellera.org for the Assertions sub-committee of the
Verilog++ committee. There should be a new web-page for this soon.
Verplex has donated the Open Verification Language to Accellera.
(See http://www.verificationlib.org/gui/content_12a.html )
So, where do the tool vendors stand on OVL and the Accellera assertion
language? Verplex's Black Tie and Real Intent's Verix are working
with Accellera to support the Accellera Assertion language extensions.
Averant's Solidify is less supportive of a standard and prefers to
stick with its proprietary language. @HDL does not support OVL, but
says they're working on an automatic translation of OVL into their
proprietary language."
- Carina Chiang of Agilent
"It seems this DAC was the year of the checker. In solving the 70%
effort snafu that the typical verification team is facing, the EDA
people are saying, "Add some checkers". We've got static checkers,
formal checkers, checkers that run and fire during simulation:
- Checkers alone will not cut it. The verification bottleneck is a
much more broad problem. It takes a combo of new tools, new
language, and more importantly methodology paradigm shift to even
begin to remove the bottleneck. So far the Random-based approach
with a Vera/e/Superlog/Verilog/VHDL is the best bang for the buck.
- Are these checkers worth it? Basically if they catch a bug, then
they are.
- Fundamental flaw: Most of these checkers are meant to be placed by
RTLer's. This is very problematic. First RTLer's chronically hate
doing verification, so getting them to learn and use this checker
stuff is not likely to happen. Second, this flys in the face of the
Second Set Of Eyes verification principle. I can make my RTL do
2+2=5 and then put a checker in that checks that 2+2=5. What I need
is a second set of eyes to read the spec and put in a check for 2+2=4
and then catch the bug. Basically these checkers are only good in
verifying assumptions by the designer. Additional checks/properties
will need to be added by the verification engineer to verify intent.
- Language,Language,Language: Each of these checker tools has its own
language. It is typically Verilog-ish, or C-ish. It hides in
comments or gets converted into real code. It is easy to learn, so
they say. This begs the question, why not just write the checkers
in e or Vera, or even an HDL for that matter?
- Checkers all cost too much. When will EDA learn that non-mainstream
tools should not be $50k a pop? I can't live without a simulator or
a synthesis tool. I can live without a checker tool. If just one of
these checker companies could flood the market with a inexpensive
tool, then maybe its little format and language would 'win', become a
standard, and then we would all be in checker paradise (OVL is free
since it is Verilog).
I bet Checkers will become like formal verification. Large companies
will be able to afford to buy the tools and have a team that runs them.
Experts at systematically checking code for wayward bugs will develop,
but the average RTL and Verifcation engineer, will not end up using
them."
- Peet James, Qualis Design
|
|
