Home > Community > Blogs > Functional Verification > ten things i ve learned about formal
 
Login with a Cadence account.
Not a member yet?
Create a permanent login account to make interactions with Cadence more convenient.

Register | Membership benefits
Get email delivery of the Functional Verification blog (individual posts).
 

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

Ten Things I've Learned About Formal

Comments(4)Filed under: Functional Verification, Incisive, IEV, formal, verifier, Enterprise

2009 is the tenth year that I've spent at least a portion of my time responsible for formal analysis products. As per my profile, my two most recent employers before Cadence were 0-In (now part of Mentor) and Synopsys. Between these jobs I consulted for eight other EDA companies, four of which offered formal products.

You would think that I've learned a few things during the past decade, and I believe that I have. Here are ten lessons I learned along the way, one for each year:

  1. Formal should be applied early – any formal tool that requires an advanced simulation testbench as a starting point can only be run late in the project when there are few bugs left

  2. Formal is about proofs as well as bugs – proving at least some assertions correct instills additional confidence in the design once bugs are no longer being found

  3. Designers should be directly involved in formal analysis – many of the best assertions arise from designers capturing the assumptions in their heads

  4. Automatic assertions can be interesting – while no tool can divine from RTL the intent in the designer's head, customers see real value in many types of automatic checks

  5. You can't neglect the basics – R&D should not focus on exotic features at the expense of language support, robustness, and core engine performance

  6. Assertion-based VIP should be a product, not a freebie – creating quality VIP is hard work that requires a serious resource commitment, so you should get paid for it

  7. Coverage is a good way to link simulation and formal – customers understand coverage in simulation, so anything that formal can do to contribute metrics is a motivation for use

  8. A good marketing story is not enough – licensing a generic formal engine from an external research lab and tacking it onto a “lint” front end does not yield a true solution

  9. Moving users from “lint” to automatic assertions to full formal is not easy – it's better to demonstrate the value of user-specified assertions and formal right up front

  10. It is possible to create a mainstream formal solution – Incisive Formal Verifier (IFV) is a successful product being used by logic designers as well as verification specialists

I learned the first nine things from my direct experience with customers and clients prior to arriving at Cadence three years ago. IFV was already a well established product at that point, so I realized when I joined that Cadence had also learned these important lessons even if some of its competitors had not.

Of course, IFV has continued to evolve since then, and I'm proud to have been a part of its ever-growing success. Now we've introduced Incisive Enterprise Verifier (IEV), offering novel links between simulation and formal analysis. We also have automatic assertions, high-quality assertion VIP products, coverage links, and the methodology and support for wide deployment.

The other day I sat in a Sales review at which I heard that just one Cadence customer, at just one of its sites, is actively using more than 200 IFV and IEV licenses. I could only dream of this sort of deployment in my past involvement with formal. I guess that we’ve all learned a few things in the past ten years!

Tom A.

The truth is out there...sometimes it's in a blog.

Comments(4)

By Stephen Meier on December 2, 2009
Tom - thanks for a decade of strong contribution to formal, and a big impact on design and EDA.  I wonder about your first statement (1).  Typically some type of testbench is required to accurately analyze the feasible input space (environment).  How does IFV help in the early design phase ?  It would seem that planning and efforts to develop assertions and environmental assumptions should be made as part of design process.  When would users actually by running formal analysis ?


By tomacadence on December 3, 2009
The ideal way to deploy formal early in the project is for each designer to specify assertions as he or she is writing the RTL for the design. Assertions on the design inputs capture his or her assumptions about the legal input space (environment). Assertions internal to the design and on its outputs capture the intended behavior of the design. Once these assertions are ready, the designer can run IFV or IEV even if no simulation testbench is available. Does this answer your questions?

By Stephen Meier on December 7, 2009
Hi Tom:  Thanks for the answer, it makes good sense.   One comment is that the quality and completeness of the assertions on the design inputs would impact the verification closure.  If the assertions are incorrect, or incomplete then you would get false positives (overconstrained inputs), or false negatives (underconstrained inputs).    In your experience do block level designers spend the effort to develop assertions at the block inputs to verify their assumptions, particularly early in the design cycle ?

By tomacadence on December 7, 2009
Mostly I see designers starting with partial constraints and adding more as needed to eliminate negatives (counter-examples) that are due to under-constraining rather than to actual design bugs. Many designers are happy to accept whatever assertion proofs they get along the way; others will continue to add constraints to try to get 100% proofs. Either way, it's important that the block-level input constraints be run as checking assertions in all higher-level simulation testbenches to try to catch any over-constraining.

Leave a Comment


Name
E-mail (will not be published)
Comment
 I have read and agree to the Terms of use and Community Guidelines.
Community Guidelines
The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.