Even the most carefully designed UVM testbench is inherently incomplete since constrained-random methods can't hit every corner case. Unfortunately, this means that even after 100% functional coverage is achieved there can still be showstopper bugs hiding in unimagined state spaces. Hence, formal verification plays a vital role in the verification of today's complex designs. Formal tools statically analyze a design's behavior with respect to a given set of properties, exhaustively exploring all possible input sequences in a breadth-first search manner to uncover design errors that would otherwise be missed.
However, many engineers are concerned about having to learn assertion languages and formal techniques, or sharing the results from formal analysis in the context of the entire verification effort. Conversely, there are a series of verification problems that are well suited to formal analysis AND which can be automated using RTL and a corresponding specification of design intent (e.g. a UPF file for low power behavior, and IP-XACT description of control&status registers, etc.) These two factors have been the motivation behind the creation of a suite of "formal apps", defined as follows:
- A formal-based tool or well-documented methodology that's focused on a very specific, high-value verification challenge
- The given verification challenge is something that can be more efficiently solved using formal methods than using simulation-based approaches
- Finally, the need to create properties or have Assertion-Based Verification knowledge is significantly reduced or even completely eliminated – typically properties can be generated by the app automatically or are provided in a pre-packaged library
The benefits of the formal app approach are two-fold:
- First, users get to leverage the power of exhaustive formal algorithms without having to learn formal techniques
- The other key benefit is that because any engineer can use a formal app, you essentially get to use the best tool for the job. So if a given verification problem is easier and faster to solve with formal, you can now use formal instead of trying to force-fit simulation or some other method.
After a brief introductory session outlining the general architecture of formal apps, in each subsequent session of the course will deep dive on a specific verification challenge and the corresponding formal application.
You are encouraged to first view Getting Started with Formal-Based Technology by Harry Foster that introduces basic concepts and terminology that should be useful by any engineer wishing to mature their formal-based technology skills.
