Going Deep Or Broad With Formal?

Whether to apply technology to semiconductor design broadly or deeply is a tough question. It hinges on what is the best way to achieve maximum ROI.

Do you want to identify hard to find bugs, and get a certain level of confidence about a block? Where should the effort be placed? Is it by going deep, meaning a team of specialists or experts must be built who can use advanced formal techniques, and do things that not everybody can do, but they can find bugs that other tools or techniques cannot find? Or is the right approach a broad one, where different applications are used that the average verification engineer or designer can get real value out of it when it comes to finding bugs?

The truth is that both deep and broad have areas of high ROI, according to. “The question could come down to how much time and investment one is willing to make,” said Sean Safarpour, CAE director for formal solutions at Synopsys. “If time is scarce, then going broad with some formal apps is a quick solution that provides a lot of value. Apps such as connectivity checking or formal register verification can be deployed within days, but can save weeks of simulation effort, as well as find bugs very quickly. They do this all without the need train anyone on ‘advanced’ formal techniques.”

There are about a dozen of such apps that verification managers can leverage with very little investment. On the other hand, if one has the ability to train an engineer on formal verification basics or hire someone with a little bit of formal verification experience, then they can deploy formal verification in a deep domain and catch high-value bugs that simulation or other verification techniques cannot find.

“In such cases, the formal owner would be writing specific properties and going after some known vulnerabilities that would find quality bugs or give management a high level of confidence,” Safarpour said.

Pete Hardee, product management director at Cadence, agreed. “Going deep or going broad is not a mutually-exclusive choice. All leading customers are in both camps to at least some degree. Formal apps that auto-generate properties are making formal verification available to general verification engineers and designers who are not familiar with SVA (SystemVerilog Assertions). For example, connectivity checking in formal is as close to a no-brainer as it gets. It’s usually much easier and more convenient than the tedious simulation-based method,” he said.

The technology is also being used alongside simulation to give formal proof that trying harder to improve a simulation testbench to get coverage on certain parts of the DUT (design under test) will not give the desired coverage improvement. Typically that can save many weeks of wasted effort per DUT, all without writing a single property, Hardee said. “This is beyond just the verification engineers. The ability to auto-generate properties to supplement structural lint with valuable functional checks (Cadence calls it Superlint) is proving very popular with designers. This makes it possible to check for arithmetic and loop overflows, FSM livelocks and deadlocks, as well as a whole range of other checks with minimal effort before handing the design off for full functional verification.”

By all accounts, the notion of ‘Apps’ started perhaps seven to eight years ago and no doubt contributed to the ‘democratization’ of formal verification. “However, while readily usable, these apps service particular verification tasks and are therefore limited in scope almost by definition,” Hardee said. “They don’t begin to challenge simulation’s position as the main workhorse of functional verification, but they do nicely complement it. What’s happened since is that all of the leading semiconductor companies are rapidly increasing their investments in deep formal, by which I mean using formal verification by writing some properties on your own.”

It’s hard to overstate the role that apps have played in the ‘broad’ expansion of the use of formal verification.

“By solving specific problems, the value of apps is easy to understand,” said Sergio Marchese, technical marketing manager at OneSpin Solutions. “Many apps require no knowledge of assertions or formal algorithms. At their best, using formal apps is as easy as running traditional ‘lint’ checks while finding significantly more serious design bugs. Apps also serve as a first step into formal verification. A user of connectivity checking may find that a few constraints are necessary to get accurate results and move on to try writing and proving a few assertions.”

Further, the use of custom-written assertions can be invaluable, as well. “In fact, both apps and custom-written assertions—from simple to high-level, end-to-end ones—provide huge value to the verification flow, both in terms of efficiency and finding more bugs,” said Marchese. “Moreover, both can do something that simulation or emulation cannot do, which is to prove the absence of bugs in the function they are verifying. Apps require little investment and are an easy choice for most projects. Formal sign-off requires expertise that many companies still do not have in-house. Whether investing in outsourcing or building expertise is worth it, depends on the project/company. For safety-critical applications like automotive or aerospace, or applications where hardware security is a major concern, both using dedicated formal apps and achieving formal sign-off, at least of specific critical functions, might be an unavoidable choice.”

Hardee pointed to a number of dynamics that have driven the rapid adoption of deep formal:

• Huge improvements in formal verification tool scalability. Designs with tens of millions, and even hundreds of millions of gates can now be processed. While gates aren’t really a good measure of complexity for formal analysis, because it’s all about state space, much work has been done increase capacity and develop much better methodologies and guidance on which design types are more amenable to formal than others. The upshot is that deep formal verification can be applied to much more of a typical chip design than just a few years ago.
• Techniques beyond pure capacity. Abstraction, property decomposition, generation of helper properties, multi-property engines, and others have improved formal performance and convergence. Much of this is automated in the tool, lessening the need for deep expertise.
• Most modern formal specialists are no longer fixated on achieving ‘complete proofs.’ Analysis tools that help engineering teams understand whether ‘bounded proofs’ (i.e., a proof that holds good for a certain number of cycles) are a good enough result.
• Bug hunting methodologies have emerged. This allows users to readily find deep Counter Example (CEX) traces. These methodologies are driven by end-to-end properties, but find difficult, high-value bugs with the full expectation that the driving property will never be proven. These methods complement simulation and often can be used to find deep corner case bugs that would be nearly impossible to write constrained random tests to find. Certain methods to perform this bug hunting regularly turns up important bugs even in mature designs, as well as contribute to coverage metrics, increasing the confidence that no bugs are left.

Methodologies matter
A significant consideration of applying formal verification technology is the ability to make it an integral part of the design process.

According to Joe Hupcey, verification product technologist at Mentor, A Siemens Business, here, both formal apps and what he calls ‘direct property checking’ deliver great value to customers independently of each other. “However, one thing we’ve seen consistently across many customers is that formal-based apps help design and verification engineers ‘cross the chasm’ and start using formal verification directly. Typically, customers get their feet wet with a formal-based connectivity checking app because the effectiveness and the ease-of-use of this flow is unquestionably orders of magnitude better than a simulation-based approach.”

Then, on the next project the engineering team tries a few more formal apps corresponding to their verification needs.

“Even though the users have been primed to expect good results, the effectiveness of ‘new’ apps regularly exceeds the customers’ already high expectations,” Hupcey said. “Spurred by the success of applying the formal apps, these teams inevitably start to look at applying formal analysis themselves. They start with ‘bug hunting’ on specific design elements, and go on to master the techniques to get full proofs of critical functionality. The key point is that this effort proceeds in parallel with running the apps on other design blocks, so the overall result is customers continue to employ both the apps and formal property checking together.”

Basically, once formal’s considerable power and benefits are introduced by a series of formal apps, there is no going back and formal becomes a permanent part of the user’s verification tool kit.

Finally, to those who say properties are difficult to write or formal tools are difficult to use, Cadence’s Hardee observed that they fall into two camps. The first involve engineers who no longer directly touch verification and are not aware about how amazingly complex it is to create UVM testbenches in SystemVerilog to fully verify today’s complex chips.

“Conceptually, they ‘get’ simulation better than formal, but they’re left behind on how complex simulation has become in reality, as well as how much can usefully be achieved with formal. The other camp are the dyed-in-the-wool UVM/constrained-random experts. They know what they know, and they’re sticking with it,” he said.