Olivier Coudert started it with his blog entry a while back. In it he had this to say “Looking at the DAC submissions this year though, I am puzzled by the overwhelming number of papers focused on increasing simulation speed and coverage, as opposed to the handful of papers discussing formal techniques. And this year is not different from last year. And the year before last. Does that mean there is a lack of innovation in formal verification core techniques?”

This just did not sound right to me and I made several comments in response to this, but I thought I should do more of a well thought out response to these claims. To help with that I made calls to my friends Holly Stump (VP Marketing) and Rajeev Ranjan (CTO) over at Jasper (disclosure – I sit on their Technical Advisory Board). Here are some of things we discussed.

Formal innovation is accelerating, not slowing down, but there has been a shift. A lot more of the innovation is now happening in industry rather than academia. Academia continues to do great work in the development of algorithms in terms of their speed, capacity and memory footprint. We have probably seen a 100X gain in these metrics over the past decade. In industry we are also starting to see a lot of innovation when it comes to the application of technology. More and more formal technology is being used, but in many cases it is now well hidden from the user’s view.

To provide one view of the success of formal, we only have to look at the numbers. If formal technology was slowing down, we would expect to see the $$$ for formal decreasing. In 2008, Jasper reported a 100% gain over 2007 revenues and while they have not yet reported their 2009 numbers, I have been told that they were good and possibly slightly better than expected. While this is only one company, this is happening during an industry downturn and this would not happen if the technology was lagging. The technology, the usability of the tools and the ROI from using formal is obviously increasing.

A lot of the advancements in formal do not result in paper being published, and in addition where those papers are published is changing. So DAC may not be an ideal indicator. First, let’s consider the premier conference for the publication of formal papers. That is FMCAD. This year there were 110 papers submitted and only 30 accepted. That is a fairly low acceptance rate indicating the breadth and quality of the work that is going on. Perhaps it is just DAC that is loosing its luster, especially in the area of verification. It has never really been strong in that field. Second, if you look at what is happening in the user group conferences, you are finding many user companies talking about what they are achieving with formal technologies. Even Jasper was blown away when one of their customers presented a paper in which formal was applied to an 89 million gate design. At the same time, you can turn your attention towards DAC, but look at the user track. There will be a number of presentations there talking about how formal technology is being used with increasing effectiveness.

Another observation that Rajeev made was that the players are changing. It used to be that two companies dominated the formal field – IBM and Intel. They would be the supplier of a large portion of the papers and they would be the people sitting on the conference panels. But this has changed. The technology is broadening and a lot more companies are involved. However, many of these companies are not so willing to publish their work or their successes.

There is also a broadening of the technology base that formal is trying to cover as well. It is no longer just about the verification of RTL designs. It is spreading to higher levels of abstraction, which would fall into the ESL space and into software that would fall into the embedded space. This means that papers on formal will be showing up in places other than just the verification tracks.

So let’s look at some of the areas of advancement just over the past year. Also, remember that this is just in one formal company, and there were probably equally bold moves in the other formal companies as well. So – please feel free to add yours to the comments in this article.

In terms of the base technology, Jasper had 4 major releases over the past year. Each release adds technology capabilities and performance increases that enables new verification problems to be addressed. For example, significant improvement in performance and capacity depends on a reduction of memory footprint. They achieved 2-3X performance increase across the board, introduced technology to make use of server farms by distributing the problem to reduce time to closure. Added proof grid that makes use of multiple algorithms spread across multiple machines and also performs task splitting to make use of compute resources available. The algorithms do not run in isolation. They collaborate on the problems in some cases such that one algorithm can help guide other so they reach solutions faster.

New algorithms are being introduced all of the time, on example of which is state space traversal. This is useful when some situations require a path to be taken into account. X propagation capabilities also new for this year.

Behavioral indexing enables a whole new range of applications even though a lot of it does not look like formal technology. This could be a huge market for the IP industry.

Debug – can take up to 50% of the verification time. Advances being made that will reduce this time. Quiet trace can help to reduce total activity in a trace so that only significant changes happen. This makes finding the root cause a lot easier. Other interactive features enable backward tracing to be easier than in the past, so that problems can be understood quicker. What if scenarios. Was this caused by … What if I disable this? Being able to answer this type of question quickly can save huge amounts of time.

Coverage – Big effort underway in Accellera. Jasper participating to create an API that would enable formal to participate in overall coverage calculations. Jasper has identified with their customers, the metrics that are important and there will announcement about the results of this soon. This is a complex issue and requires a lot of careful education. I have given various talks about this and the industry still does not fully understand the issues. This is perhaps one of the biggest issues in the verification space.

Sequential equivalence checking. This is a rapidly emerging area that is an integral part of the growing ESL space. While a lot of formal technology is common between property checking and SEC, there are new techniques and algorithms needed as well. When ESL matures and we start to see a standard flow emerging, this will probably be a highly competitive field. Today there is just a single commercial solution, but other are hovering overhead.

In Japan there is an interest in applying formal to ESL and higher-levels of technology. At a recent conference there was a Gartner analyst investigating applicable of formal to embedded software. Will Toyota be making changes based on its current problems? The application space for formal technology is rapidly growing, the technology is keeping up and even advancing and there is a lot of research happening.

So I hope we have totally managed to show that Olivier’s statements are wrong and that they were based on an incorrect view of the industry. Formal is alive, well, and growing up rapidly.

------------------------------------------------
Brian Bailey – keeping you covered