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.