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
In this session, we'll demonstrate 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: Demo
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
In 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: Demo
This session will demo assertions and results and a quick debug showing the QFL waveforms using Questa Connectivity Check. -
CoverCheck: Accelerating Coverage Closure
In this session, we'll demonstrate 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: Demo
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. We’ll look at how Questa Register Check can improve speed and completeness in your memory mapped register verification flows. -
Questa Register Check: Demo
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?
In this session, we'll 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: Demo
This session will demo the Questa SecureCheck tool and will review features including the details window, properties tab, waveform and schematic views. -
X-Check: 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: Demo
This session will demo finding X-corruption in your design using Questa X-Check.
-
-
Overview
View more Formal Verification resourcesEven 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