Automatic Formal Solutions
After a brief introductory session outlining the general architecture of formal apps, in each subsequent session of this track will deep dive on a specific verification challenge and the corresponding formal application.
-
Sessions
-
Introduction to Automated Formal Apps
This session will introduce you to Formal Apps; what they are, how they are structured and what is available today. -
AutoCheck: Push-Button Bug Hunting
This session will show how automation of assertion based methods via automated formal analysis can uncover numerous types of RTL behavioral issues, enabling immediate fixes as the RTL is being developed without the need for a testbench. -
Questa AutoCheck
This session will demo the Questa AutoCheck tool and will review features including the details window, design checks window, source, waveform, schematic, and fsm debug features. -
Connectivity Check: Connectivity Verification
This session we’ll take a quick look at the various challenges in doing connectivity verification with current methods. We’ll also look at a number of connectivity checking applications. -
Questa Connectivity Check
This session will demo assertions and results and a quick debug showing the QFL waveforms using Questa® Connectivity Check. -
CoverCheck: Accelerating Coverage Closure
This session will show how automated formal techniques can be used to keep the project moving forward by exhaustively determining the reachability or unreachability of coverage elements, grant persistent waivers to areas that can be safely excluded, and how the master coverage database can be automatically updated with the current coverage score. -
Questa CoverCheck
This session will demo the Questa CoverCheck tool and will review features including the details window, coverage checks window, and source debug features. -
Register Check: Memory Mapped Register Verification
In this session we’ll take a quick overview of memory mapped verification and some of the challenges users face with verifying these design constructs. -
Questa Register Check
This session will demo memory mapped register checkers generated results that can be debugged in the using Questa Register Check. -
SecureCheck: How Secure is your Design?
This session will show how to exhaustively prove the integrity of the hardware root of trust with your RTL and a clear text, human and machine readable spreadsheet to specify the critical storage and allowed access paths. -
Questa SecureCheck
This session will demo the Questa SecureCheck tool and will review features including the details window, properties tab, waveform and schematic views. -
Mitigating X Effects in Your Verification
In this session we’ll take a quick look at the various types of X effects and how they can impact your design. We’ll also look at some common sources of X which are the originators of these effects. -
Questa X-Check: Finding X-Corruption
This session will demo finding X corruption in your design using Questa X-Check.
-
-
Overview
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.
-
Forum Discussion - Formal
-
Issue with Defining a 2D Non-Deterministic Array in Formal Verification Property
May 21, 2025 SystemVerilog -
Query regarding witness for vacuosly passing assertions in Formal Verification
May 16, 2025 SystemVerilog