How to Become a Formal Expert and Impress your Friends and Boss!
No one ever said that functional verification was easy. In fact, from a computer science theoretical perspective verification is considered hard (NP-hard to be exact). Humor aside, each of the various verification approaches in use today will suffer some inherent limitation that will eventually reduce their effectiveness. For example, simulation-based techniques can encounter a time-explosion problem for either a large input space or large designs. Similarly, formal verification techniques will encounter a space-explosion problem on designs with a large state space. Yet, even with these limitations, many projects successfully tape out chips all the time. So, how is this possible? Well, although there are obviously scientific and engineering skills required in verification, to overcome many of today’s verification complexity limitations requires some artistry and cleverness. In this blog I plan to discuss what we are doing to help you develop skills to overcome many formal verification challenges.
The industry has experienced significant adoption of formal solutions over the past few years. One of the driving forces behind increased adoption of formal solutions has been due to advancements in formal technology. For example, in the early 1990s the effort required to use a formal tool was high, and the tools generally required an expert. In addition, the state-spaces these tools could handle were quite small. This has changed over the years, where many of the formal solutions have become fully automated. In addition, today’s formal tools can handle significantly larger capacity and state-spaces compared to their predecessors. The maturing of formal technology is driving the adoption of formal property checking on many projects today, as shown in the following figure.
However, as I previously stated, at some point in time all verification techniques will require some cleverness, or really advanced skills, to get the most out of a given solution. As an example, let’s consider simulation. The question I often pose to many project managers is “could a project team successfully develop a constrained-random, coverage-driven test without any prior knowledge to object-oriented programming, SystemVerilog, and UVM?” The answer is that it is unlikely. At least until the team develops and matures the necessary skills that are required to construct an advanced testbench. And it is really not difficult. In fact, we have developed multiple courses within the Verification Academy to help project teams master these skills.
But, what about formal property checking skills? Is it only for experts? The answer is no, advanced formal property checking skills are no longer only for experts. Anyone can develop the necessary skills required to push formal to the next level of success. Unfortunately, while there has been a lot of material published on constructing a constrained-random, coverage driven testbench and methodology, there has been a dearth of material published on developing skills for advanced formal verification. At least until now!
I am excited to announce a new video course out on the Verification Academy, titled “Handling Inconclusive Assertions in Formal Verification.” This new course was developed by my colleague Jin Hou who has a wealth of experience of applying formal property checking on real industry designs. Over the years Jin has developed many advanced techniques to address inconclusive proofs in formal verification, which she shares with you in our new course.
The Handling Inconclusive Assertions in Formal Verification course is structured into four sessions. The first session begins by reviewing tool options that can help identify the root cause of a non-converging assertion. The second session introduces techniques that can be applied to reduce the complexity of assumptions and assertions—including under-constraining, over-constraining, assertion decomposition, adding “helper” assertions, assume-guarantee, as well as how to utilize libraries of assertions that are optimized for formal. The third session introduces techniques to reduce the complexity of designs by first understanding what formal is analyzing, then this session incorporates easy ways to reduce design complexity. Detailed examples are provided for counter and memory remodeling. Finally, the forth session is what I refer to as the really advanced bag of tricks, which includes separating functions, data-independence, and utilizing non-determinism. By mastering the skills presented in this course you will maximize your usage of formal on your project and achieve results that otherwise would not be possible.
To learn more about our new and existing formal verification courses, please visit the Verification Academy!
