What's new in formal verification at DAC03
Connie L. O'Dell
June 19, 2003
ESNUG readers,
DAC '03 was my 16th DAC. I have significant background in formal
verification (model checking) as applied in industry, ABV, and formal/simulation
integration. Even in a year of tight budgets, there are some cool new
developments in these areas:
You've heard of using formal verification where it is most effective, and
simulation to cover other parts of the design?
Customers of course then ask: "So do you have a coverage tool that combines
coverage from both?"
So the punchline is that now there is such a tool, provided by 0-In.
It appears to combine the formal/verification coverage correctly, and although
the demo did not go into details of how the coverage was computed (the press
releases mentioned proof radii etc.), it did appear to be a meaningful
combination, and to be pretty easy to tell what assertions to add to improve
functional coverage. I'd like to hear from someone who has had their hands
on
this or any other coverage tool of this type.
I also see that Verisity has astutely produced an interface combining coverage
from both Verisity and 0-In for their common customers.
Nice idea, as Verisity's cross-product coverage also seems essential to many
users.
Taking no sides in the language wars, 0-In support native 0-In assertions, OVL,
PSL, and System Verilog. I also know that clock domain checking is the top
formal need for a number of customers, and 0-In has something new there as well.
Everyone who cares knows that Synopsys has had various unannounced formal/semi-
formal verification tools for a year or so.
Magellan has been announced as a semi-formal product that seems to address a
significant part of the problem. While it is semi-formal, it does seem to
include some interesting features for reducing problem size, some of which I've
had experience with in another context, so that even if it is not exhaustive, it
may still allow much of the interesting problem space to be covered.
To be brief, they seemed to have done their homework, by getting advance
feedback from some key users, so they have good answers to the common questions
about features needed in formal products.
The variety of features mentioned suggests to me that there may be multiple
possible use models, so ask about this if you get a demo, and also about
coverage.
Jasper had an interesting floor demo; at this point the people who
will have the best detailed information would be the real customer prospects,
who may have seen the full user interface. There are some unique aspects
here
also about the way the problem size is reduced, and unlike Magellan, Jasper
targets exhaustive verification.
Certainly the principals involved have impressive track records.
In favor of Jasper's approach, I have also personally verified properties that
spanned the design.
My experience is that it can be made computationally feasible (albeit
tricky), and also that it can be easier to specify and verify desirable good
behaviors that the block should always correctly perform, than to write only a
larger number of more-localized (and therefore more-easily-verified) assertions.
Perhaps in the long term, users will formally verify both local assertions and
more global good behaviors.
Both 0-In and Jasper have verification IP for common protocols for use with
formal; in my book, this greatly increases a customer's chance of success with
formal verification.
Synopsys also has an IP strategy which likely encompasses this, but I
don't know details.
@HDL and IBM both had good things to say about the new agreement between the two
for @HDL to use the IBM engine.
@HDL has PSL support in beta.
I have come up against the IBM engine in the past in benchmarking, and it is
certainly well-known for its performance.
I also like the @HDL eval report that someone posted (and those on Verix and
Solidify); any sharable eval reports for other formal tools are of course of
great interest! Haven't seen one on Verplex Blacktie for a while.
The DAC panel, "Formal Verification: Prove It or Pitch It" was quite good.
The press didn't capture the material that was beneficial to prospective users.
If you might apply formal verification, the slides by Intel's John O'Leary
provide good solid data and perspective.
Since formal verification is/will be a key aspect of assertion-based
verification, I'd also recommend more-general ABV materials from "Tutorial 4:
Assertion-Based Verification"; Erich Marschner did a nice job planning the
tutorial, all of the presenters were great, and Sean Smith's (Cisco) was
especially detailed and instructive. The need for coverage tool
improvements
was mentioned.
The book "Assertion-Based Design" by Foster/Krolnik/Lacey is a fine how-to
manual for ABV, but Lionel Bening pointed out the best part:
major chapters of realistic OVL, System Verilog, and PSL assertions
for verifying a wide variety of common design features.
No NDAs were intentionally violated in this report.
Comments or corrections welcome, especially real customer experience.
For general large-EDA-vendor insight, I highly recommend the
customer-survey-based article "Study spotlights firms, trends to watch in EDA"
at http://www.eedesign.com/story/OEG20030609S0072 .
I hope that customers continue to demand technical leadership and quality
customer support.
Cheers,
Connie L. O'Dell
Sr. Formal Verification Consultant
c.odell@co-consulting.net
(303)641-5191
Boulder, CO
___________________________________________________________________
CO Consulting, Boulder CO http://co-consulting.net
