Ten Things I've Learned About Formal

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.