( BSNUG 00 Item 6 ) ------------------------------------------- [ 10/13/00 ]
Subject: Verif., Formality, C++ Verif., A Synthesizable 'Watchdog', O-in
THE CHECK IS IN THE MAIL: On the not-so-sexy side of chip design, users
discussed the growing problems involved in functionally verifying their
chips. Peets James of Qualis gave a well received "5 Day Verification
Plan" pointing all the groupthink and politics involved with validating
a real, live design. Paul Whittemore & Frank Wong of SUN gave a detailed
talk on BFMs and C++. Others discussed Synopsys' Formality, but, oddly
there were no Synopsys Vera papers or tutorials given at the Boston SNUG.
Design weenies like myself, Kurt Baty, and Steve Golson, were found at
the "Synthesizable Watchdog Code" talk by Duane Galbi and Wilson Snyder
of Conexant. (It was a talk on making homebrew 0-in 'checkers'.)
"TB3 - The Five-Day Verification Plan 3 stars (out of 3)
Peet James presented a set of guidelines that can be followed to
develop a verification plan for your next design. Peet's presentation
slides do not have nearly as much meat as the paper, but the actual
presentation was very good. Basically, the author is a real designer
who knows that other real designers hate meetings and really hate
dealing with formal verification plans. So he designed a method to
get a bunch of cranky overworked engineers together to flesh out a
verification plan with a minimum of stress. From what I've seen so
far here at Microchip, we could use some of the ideas contained in this
presentation. The critical points are that the plan should be put in
place as soon as possible in the design cycle and that it needs to have
buy-in from everyone (which means soliciting everyone's input). This
is a good read."
- Brian Fall of Microchip Technology, Inc.
"VI) Verif Planning and Formality
A) 5 day plan: My paper. People seemed to realy like the aim of the
paper of focusing more on how to make the plan and get engineers
to buy into it. They also liked the yellow sticky method. Good
questions both afterwards and during the fireside chat.
B) Formality: Military/Space redo of a PowerPC core. Good divide
and conquire approach with scripting. Easy iteration turn around.
RTL to RTL compare. Debugging, which is usually the hassle of
formal verification seemed smooth. Overall results were good.
Time saved over pure simulation.
VII) Fireside chat: This new feature of SNUG. Had each presenter
standing by a paper easil. People came by and asked question.
I had a steady stream of people. It was fun and informative. It
lasted almost an hour, and I would have liked both a stool to
sit on and a beverage. Gregg Lahti was giving away free Tcl code
on a floppy. He had 'FREE CODE' written across his easil. Not to
be out done, I wrote in large letters 'FREE BEER'.
- Peet James of Qualis Design
"Formal Verification:
These tools compare the RTL with the Netlist, then report differences.
The compare coupled with static timing checks in Primetime can replace
netlist simulations. This allows the functional simulations to remain
in the behavioral/RTL world which run much faster than the structural
netlist.
Thoughts:
It sounds good in theory, but everyone I talked with who considered it
said they didn't have the guts to go without structural simulations.
We may want to try this Post-[Project Name Deleted] or on a test run."
- an anon engineer
"V) High Level Verification
A) Random C based Verification: Paul Whittemore & Frank Wong of SUN
1) CVI is their in-house tool that uses C to accomplish what Vera or
E does in producing a more random verification approach.
2) The goal of the CVI environment is to use a C++ object oriented
approach that will allow for quicker and more effective testbench
generation.
3) DUV still has some vlog BFMs. C++ BFMS hook to the vlog BFMs. C++
API is used to direct the BFMs. The BFMs are low level, mainly
handshaking. Higher functions are done by the C++
4) Decomposition: Logical breakdown of the Verification pieces to
divide and conqure. (BFMs, MON, TC, DUV, CHK, GEN)
5) Layering: Levels of abstraction to enable average testcase writer
to generate tests fast. Still can access lowest level to make
special tests. Most test ment to be automatic.
6) Transaction Generators: Private and Public coding style via header
files that hide the overal complexity to the average user. Random
elements with autochecking and parameters are builts. Some
parameters intialized at start & remain, others change on the fly.
7) Constraints: Has E and Vera type mechinisms to defualt, weight
or hardcode parameters.
8) **** Used UML class hierarchy diagram to show the OOP interaction
between classes and methods.
9) No coverage built in.
10) Test Control: Uses a FSM model to run the tests. Master FSM,
with sublayers of other FSMs. Has arbiter built in. Chose this
over thread driven control.
a) Load BFM data
b) Program I/O
c) Check results
11) Test manager: handles random test parts."
- Peet James of Qualis Design
"Formal verification: should we invest in this, especially since we will
be doing RTL modifications for scan and power savings? Main use is to
formally verify RTL source code against a gate level 'equivalent'.
This can be done at various points along the design flow, but is most
important after we have added all the post-synthesis junk like clock
tree buffers, scan logic, etc. These tools will *not* formally verify
gate level schematics with any transistor level switches."
- Brian Fall of Microchip Technology, Inc.
"B) Synthesizable Watchdog Code by Duane Galbi of Conexant.
I found this paper the most interesting. It describes sort of a
poor man's 0-in technique of putting in little watchdog checkers
and reporters throughout your RTL code. This code is done in such
a way as to not cause any logic in DC.
1) Method: if done right, does not even need translate on/off
constructs in the code. DC will easily ignore.
2) Preprocessor used to implement the technique. Available at
http://www.ultranet/~wssnyder/veripool
3) Watchdog code is put into a $ system call. The are about 5
(more used by the author) different calls. Each has parameters
that are fed to the system call. It can do notes or warning or
errors, but also more advanced checking. The actual $assert
commands are kept to one line, in order to not screw up line
numbering.
4) Has runtime message levels, so you can turn stuff on and off.
5) Simple and easy enough so that RTLr's can install as they write
code. Has to be simple and transparent
6) Examples are fsm trackers, counter checkers, etc.
7) Poke holes: You can put these in the behavoir models as well,
but being a RTL entry item, they still sort of promote the
old school methodology of doing RTL first and verification
2nd. Concurrent Verification and RTL would not reap the benefit
of any of the checkers firing, until the RTL was fully
incorporated."
- Peet James of Qualis Design
|
|
