The Early Bird Catches The Bug Using Formal

It has been suggested that formal might replace simulation, at least in some parts of the design flow. Not likely! The question is, how can formal be layered on top of simulation flows to improve coverage and schedule?

The way formal is being used at the larger semiconductor companies is evolving. In many of these companies a small team of hardcore formal experts are employed across different projects to try and find the toughest bugs. Armed with powerful formal engines and expertise on how to apply them to tough corner cases, they do indeed add a layer of verification depth right at a point where it counts. Often that point, is at the end of the verification flow.

However, this just scratches the surface of the potential of this technology. Formal can improve a number of phases of the verification process, but this work can’t be left to a specialized few. It has to be used by the entire project team, and across the entire process.

I recently had the opportunity to chat with a number of these expert users from different companies around the world. Not surprisingly, they had a range of opinions about best practices for formal tools and the kinds of assertions and constraints they apply to design code. However, there was one universal comment they all made about formal – essentially if other engineers could adopt it, even on simpler tasks with easier use models, they would see significant improvements. Formal used early in development would more easily eliminate bugs that are painful to track down later.

Now, one might think that these experts would prefer that they keep all this good formal stuff to themselves. This is not the case. Most of them actively participate in training, conferences and other events aimed at proliferating the technology. They said that they would like to see greater usage throughout the teams with which they work, and fully believe that if this happened the verification task as a whole would be improved greatly.

So what is going on here? We know that formal is used by expert teams on the toughest verification problems. We also know it is used by many developers under the hood in a range of formal apps – automated solutions that require no knowledge of manual assertion authoring. Is there a middle layer of engineers that could benefit with just some simple assertions? The suggestion is absolutely yes!

What would it take to make this happen? I posed this question to the experts as well, and on this they were a little more divided. Summing all of their answers (and applying a little rounding), here’s a list of ideas:

First, make it easy to create those assertions, at least to get the engineers up on their feet. Assertion abstractions or templates can be provided to make their creation easier. Alternatively, a cookbook or other examples on common code structures could be provided. Learning by example is always easiest. Coupled with this, guidance on what components of the block under verification are best tackled with formal rather than simulation. Why also is important.

Second, a new mindset must be adopted by the team to combat the sense that formal is hard to understand. In many ways, formal is easier than many tools, but users need to have a good feel for what is going on under the hood. Anything that can be done to demonstrate this would go a long way.

Third, anything that can be done to make using the tool feel familiar is important. Making the debug environment look more like that of a simulator’s would help. Integrating coverage results would provide a sense of how a complete environment would work.

Finally, engineers need some free time to experiment with the technology, which maybe the hardest item on the list!

To make this happen requires expert formal vendors working together with expert formal engineers. However, the benefit is huge and clear, and it’s worth a little effort. Engineers – let’s give it a shot!