Thought Leadership

Learn Formal the Easy Way

By Joe Hupcey III

The sight of kids going back to school can prompt feelings of joy and renewal – or trigger less pleasant memories of painful academic trials. I regularly see this dichotomy play out with formal verification – because everyone wants exhaustive verification, people generally want to learn more about formal property checking flows and tools; but they either don’t where to start, or they are afraid that the learning curve will be protracted and confusing. Good news: this September there are a variety of upcoming programs – as well as on-demand offerings available right now – that will help anyone who is familiar with VHDL, Verilog, SystemC, or C++ learn the basics of formal.

Tuesday September 7, 2021: DVClub Europe, “Formal Verification Adoption Made Easy

Two highlights of this event include presentations by:

Logistical note: this event starts at Noon BST – that’s 7am Eastern, 4am Pacific. Naturally it’s best to tune-in live so you can ask the presenters questions, but if the time zone difference is too great for you please do register so you will quickly get the link(s) to the recordings.

Tuesday September 28, 2021: Formal 101 – Exhaustive Scoreboarding and Data Integrity Verification Made Easy

“Scoreboards” are a common technique to verify the safe passage of data through a DUT. Conventional wisdom claims that you can only do this with simulation because formal verification only works for control logic and cannot be used for any datapath verification. Not true! In this webinar Senior Principal Product Engineer Mark Eslinger will show how you can quickly and easily setup and run exhaustive data integrity verification with a formal-based score boarding analysis with IEEE standard SVA properties.

And in case you missed the earlier installments of our “Formal 101” series, they are available on-demand now:

Formal 101 – Setting Up & Optimizing Constraints

Conceptually, constraints on formal analysis serve the same purpose as they do in constrained-random simulation: they focus the analysis on a specific range of inputs that the DUT is likely to encounter. However, because formal analysis is fundamentally different from simulation under-the-hood, there are several twists on how you setup and manipulate constraints for property checking vs. a UVM testbench simulation. In this webinar we will show you all the tricks of the Formal constraints trade so you can rapidly bring-up a formal testbench.

Formal 101 – Basic Abstraction Techniques

Formal verification algorithms can struggle to read-in and analyze DUTs with very large state spaces. Specifically, circuit elements like counters and memories can introduce a lot of state bits and sequential state depth that can bring a formal analysis to a grinding halt. The solution is to “abstract away” such parts of the DUT by either swapping in simplified models of these elements, or by safely removing them completely (electronically, without touching your golden RTL source code). In this 35 minute webinar Senior Principal Product Engineer Jin Hou will teach you about the types of DUT constructs that commonly cause trouble for the formal analysis, and how to apply time-tested techniques to safely abstract them away so that the formal verification run can rapidly reach closure.

Last but not least: there are all the formal-centric courses on Verification Academy.

Have a great day at school!


Joe Hupcey III,
for the Siemens EDA Formal Verification team

Leave a Reply

This article first appeared on the Siemens Digital Industries Software blog at https://blogs.sw.siemens.com/verificationhorizons/2021/08/31/learn-formal-the-easy-way/