Just before the Christmas holidays I had a phone call with Kathryn Kranen President and CEO of Jasper Design Automation. You can hear the entire interview by clicking on the appropriate link below. What follows is an overview of the call.

How have formal tools evolved since you came to Jasper?

Kathryn joined Jasper on a full time capacity in March 2003, but started working with the company in November 2002. At that time the capacity of tools and algorithms was the major problem. Engineers with formal techniques backgrounds could, at most, verify circuits with several hundreds of flip-flops. Capacity now is in the tens or even hundreds of thousands of flip/flops in the cone of influence.
Solvers have evolved significantly and the way they are combined together has improved to form a proofs grid.

Abstractions are now "under the hood" of the products, and algorithms encapsulate abstractions making the use of formal tools in the reach of practically all designers.
Top level IP can now be run in Formal Verification, including post silicon debugging.

Applicability of formal. In the early days one could verify at most an abstracted model of a cash controller. Now you can run formal on critical properties that are about deadlock or starvation for protocol verification. But formal techniques are also being used in architectural verification and to verify the power management unit for low power architectures. Formal tools now can even support asynchronous design verification.

Are there "return on the investment" stories you can share?

Assertion based verification seen simply as a methodology upgrade does not produce, in general, significant short term results in cost savings. Instead companies should look at the technology as a way to lower specific development costs. Companies that quantize the use of formal are experiencing greater productivity and higher quality of results.

Is formal becoming less of an “experts-only” club and more of a mainstream verification technology?

Jasper has seen the following distribution of users.
Engineers that run formal as their primary job function make up about around 25-30% of users.
Verification engineers that use formal from time to time count for 35-40% of the users base.
And engineers that use formal tools for design exploration are about 35% of users

What are the growth markets/applications for formal?

Many use models now exist. Jasper is targeting large accounts and plans to grow by having at least 50 large accounts on its customers list. Of course small companies are welcome but the marketing effort is toward the large users.

Formal techniques are becoming B2B enablers. The use of formal techniques for IP certification and comprehension for example is growing and becoming an established tool for IP exploration.

When we talk about markets outside traditional EDA application, formal software verification is a research project at Jasper. Security is another market, as well as safety.

MP3 Download: 

Jasper.mp3