( ESNUG 350 Item 11 ) -------------------------------------------- [4/27/00]
From: Greg Mokler <gmokler@dal.asp.ti.com>
Subject: A Review Of The Recent Verisity (Specman) User's Group Meeting
Hi, John,
You said you wanted more user input about Vera and Specman. Here's my
Trip Report for the recent Verisity (Specman) User's Group meeting.
Verisity's first user's group meeting was held in San Jose on April 12 - 13.
About 74 attendees actually showed up out of 115 who registered. Of these,
over half were from companies located outside the valley, and about 20
percent from overseas.
Verisity was represented by CTO and founder Yoav Hollander, VP of Marketing
Francine Fergeson, Yaron Kashai who is their expert on Formal Link and it's
use with formal verification tools, and Andy Lynch, formally of Surefire
and the author of the coverage tool SureCov, which Verisity acquired along
with SureSolve when they bought Surefire last year.
Yoav was anxious for input from users on what the company is doing wrong,
but went away disappointed. Although there were definitely some power
users there, most of the attendees were fairly new to the tool. The depth
of experience to provide the kind of feedback he was looking for just wasn't
there this year. Hopefully, this situation will change as the industry gets
more experience with Specman Elite. The Verisity folks also expressed their
desire to see future meetings being much more user driven, and has set up a
steering committee of users from attending customers to drive this.
Presentations were primarily from users, but also included several from
third party developers, outside consultants and one by Yoav. The complete
presentations are NOT available on Verisity's web site at present. In his
keynote address, Yoav called the current state of Specman Elite a "good
start" which has mechanized the easy part of verification, but said that a
lot of methodology (and the features to support it) still needs to be
invented.
Presentations
Presentation #1 Technology Roadmap . . . . . . . Yoav Hollander, Verisity
The next major release, 3.3, is scheduled to ship in late August and will
include several badly needed enhancements. Waveform viewer integration will
allow interactive tracing of events, expressions, log messages, and threads
without having to modify loaded e modules. Initial viewers supported will
include Signal Scan, Virsim, and Modelsim. Obviously, the ability to
graphically see the relationship between signal transitions and event
emissions will be a big improvement over the current event chart "feature".
For VHDL coders, this release will provide better support for the interface.
Calling VHDL procedures, the ability to force signals directly, and VHDL
strings will be supported. Also, for Modelsim only, simulator commands can
be sent to the simulator from "e?".
Future enhancements on the roadmap are support for distributed simulation
(whereby separate threads of a sim can be run on different machines), a
Java-based GUI for the coverage tool, and a "complete facelift" for
Specview. Also in the works is automatic feedback of coverage to
generation. The tool will be called Coverage Maximizer and will have two
parts. The first part will analyze the design architecture and existing
test files to intelligently identify and define coverage items. This should
help users get started on a coverage plan for their design. The second part
will evolve over time. The initial implementation of Coverage Maximizer
will be to provide automatic generation of test files (constraints to
overlay) which can then be run separately to fill coverage holes left by
previous runs. There is currently a debate within Verisity about whether or
not to provide a reactive test generation capability in which Coverage
Maximizer iteratively reads coverage metrics and generates new tests
on-the-fly to fill coverage holes.
Presentation #2 Transitioning an Internally Generated Testbench
to Specman Elite. . . . . . . . . . . . . Robert Quist, HP
Presentation #9 Replacing an Internal Tool with Specman Elite
. . . . . . . . . . . . . . . . . . . Kevin Jones, Rambus
These folks made the "leap of faith" to abandon a great deal of existing
infrastructure to adopt Specman Elite as their verification environment
despite the fact that the existing test benches had worked extremely well
on previous projects. Both speakers agreed that the results were well worth
the pain of doing so.
Robert Quist of HP sighted various reasons for this decision. The current
environment required a large amount of maintenance which could be more
economically done by a third party company. Also, the need for a "dramatic
increase" in the amount of random test generation was mentioned. Robert
presented an extensible test bench architecture which leverages the use of
verification components which were designed for module level testing and
then "bolted on" to the system level bench. He also shared some specific
coding practices that were compiled from their project post mortem.
Kevin Jones of Rambus sighted similar considerations. As a small team, his
verification staff lacked the bandwidth to maintain a tool written in LISP
by people who were no longer available to help. He sighted incremental
migration from the old tool to Specman Elite as the reason for their
ability to stay productive during the process.
Both speakers also emphasized the advantages of having access to metrics
for measuring and reporting status of the verification effort to management
via Specman's coverage features.
Presentation #3 Generation for CPUs . . Ori Chazan, National Semiconductor
Classic techniques for obtaining test cases for CPU designs present
problems: using existing software applications, assuming that they exist,
typically provides only partial coverage of the design's test space, while
writing directed tests may miss or fail to identify many corner cases. Ori
presented two methods for generation of random tests for CPU verification.
In the first method, which he called "correct by construction" a program
(list of instructions) is generated up front prior to running the HDL
simulator. Constraints are defined which ensure that every generated
instruction is legal, both syntactically and semantically. Since the
"legalness" of an instruction depends upon the current state of the CPU
registers and memory, this approach requires that the full state of the CPU
be maintained within the Specman environment and updated after each
instruction is generated. By using this method, then, every instruction of
the generated program is guaranteed to be valid "by induction". Ori's group
found that this approach can be problematic: in many cases, the definition
of constraints to ensure that only legal instructions are generated are too
difficult to express. Under these conditions, an alternate method of
instruction generation is needed. In Ori's second method, a candidate
instructions is generated using a less ambitious set of constraints that
ensure the instruction is syntactically legal & also that state-independent
semantic considerations are accounted for during generation. Each
instruction is submitted to the simulator, then, based on information from
the simulator, the remaining conditions for "legalness" are checked. If
some constraint has been violated, then the candidate instruction is
rejected, and the simulator state is rolled back, otherwise, the instruction
is added to a list (to preserve the program) and the simulator state is left
as is.
Presentation #4 SoC Verification with Seamless . . . Brian Bailey, Mentor
Brian discussed work being done by the VSI Alliance. This system level
working group is trying to define rules for using, exchanging, verifying,
and integrating Virtual Components in an effort to make design reuse more
practical. He then gave a presentation of Seamless and it?s use with
Specman Elite. From the work that's been done by Verisity and Mentor,
Specman can access S/W symbols, and memory state of a processor as it
fetches and executes object code.
Presentation #5 Denali/Specman Integration . . . . . . . Sean Smith, Cisco
Sean Smith has been using Denali memory models in conjunction with Specman
for several years. He discussed the mechanics and benefits of this
methodology. He says that the ability to access memory from "e" and to
have memories generate callbacks to ?e? has raised his ability to verify
systems to another level. His arguments were extremely convincing. Anyone
using Specman to verify a system with external memories or large internal
blocks of memory should take a serious look at this presentation! Also,
Sean's paper included a web link where example code can be downloaded:
http://netmediasolutions.com/verification/oo_verification_examples.zip
Presentation #6 How to Build an eVC . . . . . . . Janick Bergeron, Qualis
Because verification requires a larger effort than design and is not
subject to limitations of target technology, testability requirements, or
synchronous design rules, Janick believes that reuse of verification
components is essential and practical. He presented a number of specific
practices which must be followed to quickly produce a good reusable
component, class libraries, Specman coding guidelines, etc.
Presentation #7 RTL-based Object-oriented Models . . J Marc Edwards, Cisco
Since the industry is trying to move to higher levels of abstraction in
design using oo languages like C++, it makes sense to consider "e" as a
candidate: an oo language with the ability to handle temporal concepts is,
like Specman, a natural for this application. Also, the generation engine
could be used to generate objects on-the-fly at the architectural level,
thus bringing automation to the exploratory phases of system design. Cisco
has funded some university research to develop an "e"-to-Verilog translator.
The initial approach will be to restrict "e" to a subset of constructs
which are easily mapped to Verilog. Later, more abstract concepts such as
inferring memories from "e" data structures will be explored.
Presentation #8 How to verify an ATM Switch . . Heath Chambers, Consultant
Heath discussed his experiences using Specman to verify a large ATM switch.
This was a classic application of the tool that really demonstrates it's
capabilities. It was also a good presentation of some of the typical
mistakes that are made when using the tool for the first time. The
impressive part is that the project was very successful despite all the
mistakes. More experience with the methodology promises big payoffs!
Roundtables
There were also a number of roundtable discussions covering various topics.
Several interesting developments were discussed:
- "e" language standardization - A steering committee will be formed in
the next several months to drive this effort consisting of parties with
a stake in the language, including "two major EDA vendors".
- Porting of temporal language to verilog - Verisity has agreed to
contribute their temporal language to OVI.
- Formal Link update - Verisity sees a need for a unified environment
wherein a single source drives both simulation and formal verification.
Taking advantage of the fact that a subset of "e" already has formal
semantics (temporal language, etc.) and that model checker properties
are, presumably, easier to debug using simulation. Verisity plans to
simplify the model checking methodology by providing synthesis of "e"
to model checking properties. Formal Link is a tool that Verisity
demo'd at DAC last year as a front end to SMV - a formal verification
tool developed at Cadence, UC Berkeley Labs. It is currently being
integrated with a commercial model checker from a "major EDA vendor"
(hmmm, how many major EDA vendors have these products? ) and will be
announced soon. The tool takes Specman temporal checks as input and
synthesizes model checker queries.
Lowlights
Considering that this was the first user's group meeting, there really
weren't a lot of negatives other than the users' aforementioned lack of
experience with the tool. The meeting had a day and a half of
presentations/roundtables (which could have been condensed down to a day)
and, since it was scheduled in the middle of the week, consumed about 3 days
of time for those of us who were coming in from out of the area. So maybe
the timing could have been better. Verisity has already said that next
year, the program will be extended to 2 full days with some advanced
training sessions.
One of the users in the audience asked Janick Bergeron why he recommended
Vera over Specman at the last meeting of SNUG. We all wanted to hear his
answer, but never got one.
- Greg Mokler
Texas Instruments, Inc. Dallas, TX
|
|
