The Other Side Of Formal

It’s natural to think of formal analysis as a ruthlessly effective bug hunter and verification tool. But as the following case study from Homayoon Akhiani, presented at the Jasper Users Group (JUG) meeting shows, customers are using this approach to increase their SoC’s performance in ways that are very visible to the end-user of the part. Such visible improvements — in this case, minimizing the length of SoC reset — is a key factor for NVIDIA’s success in winning sockets for their parts. Here are some highlights from Homayoon’s presentation:

DUT in question: A state-of-the-art CPU+GPU SoC comprised of many many IPs, targeted to the mobile market.

Project Goals & Strategy: Minimize SoC hardware reset time as much as possible.

• It’s a given that systems must hold reset long enough to ensure that all the hardware resettable flops have been reset and the design is quiescent.
• However, long reset times can negatively affect the end-user experience.

Corresponding Technical Challenge:

• As the speed of the boot time of mobile SoCs becomes important, it’s necessary to know the bare minimum number of cycles needed to reset the chip.
• Unfortunately the number of cycles to hold the reset signal in a complex design is very difficult to calculate. It’s not always obvious even which IPs are the “long poles in the tent.” This generally leads to longer than necessary reset times as people tend to pad-out reset as a precautionary measure.

Key Tasks:

• Find the area(s) of the design that take too many cycles to reset.
• Consider and analyze better reset methodologies for the offending IPs (decide between dedicated hardware reset vs. propagated reset vs. software reset).

Formal environment and tools:

• Input: RTL
• Jasper App used: the Visualize dynamic waveform manipulation and debug tool included in the JasperGold Formal Property Verification App (“FPV”). This tool can mathematically determine the logic path that takes the longest time to reset.
• In addition, the App supports “What If?” analysis that enables the engineer to manipulate signals within legal limits on the fly, thus enabling engineers to instantly explore alternative reset implementations without having to recompile.
• Optional: Jasper’s Design Coverage Verification App (“COV”).

Methodology

• Explore each IPs reset sequence with Visualize, which identifies the internal logic that takes the longest time to reset.
• The tool enables black boxing of everything except the reset signaling and logic.
• The tool also has capabilities to properly account for the relationships between reset and clock signals.
• Jasper’s COV App can also be used to detect if you have a “good” reset – a “bad” reset signal is evident from the low coverage of its bounded proofs.

Results

• In the past year, this analysis has identified many functional bugs and inefficient RTL coding that led to extra-long reset times – giving NVIDIA’s end-products a demonstrable competitive edge.

 Types of bugs found

• Design optimization: Reset to some areas changed to do faster reset.
• Gated clock not clocking during reset.
• Simulation environment bugs: Extra-long reset simulation in gate simulation.

Taking a step back, this success story is but one of 14 user presentations delivered at the Jasper Users Group meeting. The paper topics were a mix of novel, “pure formal” verification methodologies, and deep dives on specific apps like the story recounted above. They are posted on Jasper’s Formal Expert site (registration required).