VC Formal SIG Virtually Conferences in Europe

Pratik Mahajan, Synopsys VC Formal R&D Group Director, kicked off an absorbing event featuring talks from multiple customers in Europe. He spent some time on formal signoff, an important topic that I’m still not sure is fully understood. Answering the questions “OK, we did a bunch of formal checking but how does that affect total design signoff? And how does this complement dynamic signoff?” A lot of progress has been made here, in areas like formal core coverage, combining formal and dynamic coverage together and accelerating debug through ML-assisted bug triage. Also using formal to accelerate and strengthen low power and safety verification. Lots of meat in this VC Formal SIG.

Keynote on formal today in production verification

Mirella Negra Marcigaglia, Verification Manager at ST Micro Catania, gave the opening keynote on how formal fits into today’s verification challenges. She pushes formal first in development because it’s faster (no TB needed), simpler to use through apps, easier to reuse and of course exhaustive. It’s not perfect: we still need to wrestle with convergence challenges, size constraints, how comprehensive are our properties and whether anything is over-constrained. Mirella makes a very interesting point in her closing slide, that formal skills should be taught much more broadly across design groups. She’s responsible for both, yet in her view formal is easier to pick up than UVM, so should not be limited to a formal-only group. Times are changing.

Modern formal applied to the FDIV bug

In the ‘90s, the Intel FDIV bug catapulted formal from an academic curiosity to a commercial reality. Max Freiburghaus of Imagination Technology shows how this bug would have been caught by modern formal equivalence checking, here in VC Formal DPV (datapath verifier). He goes into detail on the SRT algorithm, showing how approximations inherent in the method can lead to hard-to-reach corner case bugs. And how DPV can find these. You’ll have to concentrate carefully to follow the argument, but worth the effort for a nice demonstration.

When is a bounded proof good enough?

Anthony Wood of GraphCore presented on this topic, which always trips us up. Answering this question isn’t trivial. Perhaps you should increase the proof depth. But that may not be the smart option. Some elements, like counters and memories are between hard and impossible to test exhaustively. And not worth the effort because the great majority of states differ insignificantly from others. You want to cover boundary conditions, unique combinations where bugs may lurk. Anthony talks about a few examples and how formal testbench analysis can help navigate the possibilities. He also throws in a couple of teasers on how formal can help in continuous integration and continuous delivery flows. Nice! Disruptive changes often create new opportunities.

Ultra-low power verification

Another popular topic. Karine Avagian, R&D Formal Verification Engineer and Joakim Urdahl, Sr. Engineer in Verification Methodologies, both at Nordic Semiconductor talked about their work in this area. Joakim has strong background in formal, however adoption in Nordic is relatively recent, so this section covers their first steps to a foundation for ULP checking. Emphasis is on complete property checking, defining properties to describe the complete input/output behavior of a block.

This is an interesting study of first steps into using serious property checking (as opposed to apps). They start with the spec for a block (a UART), define a conceptual state machine for the behavior, then write properties they expect to apply based on that description. Even though this was a learning exercise, they found bugs in the implementation and opportunities for further ultra-low power optimization. For a part that has been in production for quite a while. (Note to self – already in production for years doesn’t mean it’s bug-free.)

Formal versus simulation

Finally, Paul Stravers from the Synopsys Solutions Group presented on eliminating block level sims using formal signoff. This is an eternal quest in formal, their ‘impossible dream’. Which might attract derision, but I like this thinking. We wouldn’t get anywhere interesting without moonshots. Even if/when these projects fail to reach their hoped-for goal, they still make important new discoveries. More power to them. Incidentally, an HSCA is a cluster adapter, commonly used in Ethernet logic. Took me quite a while to figure this out.

You can register to watch the complete VC Formal SIG HERE.

Also Read:

Key Requirements for Effective SoC Verification Management

Techniques and Tools for Accelerating Low Power Design Simulations

A New ML Application, in Formal Regressions