Getting Formal With Power

By Ed Sperling
Formal methodologies have always been an important tool in the verification engineer’s toolbox because they often can pinpoint bugs faster and with more accuracy than other verification approaches. The problem is that most engineers don’t know how to use them, and understanding this technology to a proficiency level requires a learning curve that most engineers consider painful.

The pain isn’t going away. Many engineers still find assertions difficult to work with and understand. But what is changing is that the tools are now required for debugging nearly all complex SoCs at advanced nodes, and they’re being applied to areas that are new even for those well versed in formal methodologies. So while the learning curve is still steep, it’s becoming a required skill.

“Formal verification has been around for a while, but it’s getting much wider use now,” said Qi Wang, technical marketing group director for solutions marketing in Cadence’s low power and mixed signal group. “One of those areas is low power verification, where you use UVM assertions. With simulation you can still find a bug, but it takes between 3 and 10 times longer. With assertions you can find when the failure occurs and the exact location.”

Some of those assertions can be created automatically from power intent files, particularly CPF, which uses isolation sequencing to shut off power domains. That can be cross-checked against SPICE models, Wang noted.

“We have three customers adopting a large company’s spec,” Wang said. “But it’s hard to embed assertions in a spec. They have 10 voltage islands, which at the system level is 100 possible states. They need a lot of assertions to specify what is the legal mode of operation.”

Cadence isn’t alone in seeing this increased interest in formal tools for finding power bugs. Oz Levia, vice president of marketing and business development at Jasper Design Automation, said his company has been approached by several customers in recent months about using formal tools in relation to power.

“They’re not looking to use it for structural coherency,” he said. “It’s the functional aspect of powering up and down. If you have a half-dozen power domains and combinatorial sequences you can either prove it’s working correctly or find a bug where you get unexpected values. Even if your sequence is correct you may have unexpected latching or timing between sequences.”

With one power or two power domains this is manageable with a spreadsheet. As the number of cores, processors, power islands and different voltages increases, understanding the potential interactions is almost impossible without automation. And finding bugs in the design is even harder.

The other side of formal
But formal methods also are being used by EDA companies internally to reverse-engineer some of the problems and then create tools to work around those problems.

“The challenge is expressing the problem the right way so you get an answer that’s useful,” said Mike Gianfagna, vice president of marketing at Atrenta. “We spend a lot of time in expressing the problem. The trouble with formal is that it’s difficult to use. You need to understand formal and how to express it mathematically.”

Atrenta has targeted memory with this approach, which has generally been ignored in power reduction. In logic, the power reduction generally involves library files. But in memory, there are no such libraries. It comes down to searching out redundant read-write, light sleep/deep sleep functions and eliminating them one by one.

“The problem is that no two memories are the same,” said Gianfagna. “They differ from vendor to vendor and from one technology node to the next even with the same vendor. Standards would really help in this area. Right now we do it one at a time. What formal also allows us to do is to analyze finite state machines and look for dead code.”

The future
Formal methodologies and tools have been around for decades. They are employed by most major chip companies, although the number of engineers using these kinds of tools is beginning to ramp up quickly as complexity increases. With more use, there also are likely to be more uses—most notably in power, and eventually in software where this kind of technology has been largely ignored.

Backers of formal have been predicting rapid uptake in the market for the better part of a decade. It still lags other areas, but what’s changing is the number of people who see a value in this kind of technology. Now the question is when that recognition will turn into widespread adoption.