Recap: Decoding Formal Club, Spring 2017

What better way to celebrate the arrival of spring than another meeting of the Decoding Formal Club! The Decoding Formal Club is a forum for formal verification enthusiasts, pioneers, leaders and friends who work to promote the sharing of ideas, advancement of formal verification technology, and adoption of formal sign-off methodology within the industry. On Tuesday, March 21, the club met to hear presentations from Oski, Nvidia and Arteris.

Vigyan Singhal, Oski CEO and formal verification visionary, started us off by introducing the concept of architectural formal verification. Some system level requirements are, by their very nature, well suited for formal verification. Cache coherence, absence of deadlocks and security features are examples of things that we would want to verify with formal. However, the complexity of today’s systems makes it impractical to do so at the RTL level. Instead, Vigyan talked about how Oski uses abstract components to build a system-level model that can be successfully analyzed by formal verification.

Many in attendance liked this approach but also noted the challenge of ensuring that the behavior of the abstract components matches the implementation in RTL. Vigyan explained how Oski’s methodology has that covered when the properties of the abstract models are validated against the RTL designs to close the loop.

Dovetailing nicely with that, Siddartha Papineni, senior formal verification engineer at Nvidia, presented a case study of using the architectural formal verification methodology described by Vigyan. Siddartha’s talk was about verifying system-level cache coherence. He talked about the challenges of verifying a coherency control system that communicates with compute clusters that have different interface coherence protocols, yet share the same memory contents in their respective caches.

The results were that Nvidia was able to prove coherence properties of the system as well as compliance with the interface protocols. Siddartha also presented examples of high-value, architectural bugs found and fixed through this process.

Continuing with the theme of cache verification, the next presentation was about formal sign-off on the RTL design of a configurable cache controller. Parimal Gaikwad, hardware design engineer at Arteris and Kamal Sekhon, formal verification applications engineer at Oski tag-teamed to present this case study.

Parimal talked about how Arteris completely replaced block level simulation with formal for this design. He described how the design was highly configurable, with complex interfaces and how it was required to support many combinations of events in parallel, such as pipeline stalls, replays and error conditions.

Kamal then shared how a formal testbench was built to verify this design. She described the techniques used to overcome complexity barriers such as decomposition, use of symmetry, reset value abstractions and cut-points. The result was that the design was fully debugged with formal and no bugs were discovered in this block during system-level verification. In addition, Parimal talked about how much time he saved by triaging the bugs using formal traces when compared to traditional debugging with much more lengthy simulation waveforms.

Many thanks to Synopsys, the event sponsor. Representatives from 18 different companies attended the meeting, including Nvidia, Qualcomm, Intel, Apple, Google and Cisco. If you missed it, be sure to be informed about future Decoding Formal Club events and more by signing up for the Oski newsletter.

Tags: "Decoding Formal" Club, architectural formal verification, best practices formal verification, formal analysis, formal sign-off, formal verification

This entry was posted on Wednesday, March 29th, 2017 at 2:14 pm. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.