Questa Formal Verification
Overview
Questa formal apps boost verification efficiency and design quality by exhaustively addressing verification tasks that are difficult to complete with traditional methods, and they don’t require formal or assertion-based verification experience.
The Questa Formal Verification Apps complement simulation-based RTL design verification by analysing all possible behaviours of the design to detect any reachable error states. This exhaustive analysis ensures that critical control blocks work correctly in all cases and locates design errors that may be missed in simulation.
Questa Formal Apps can be used as soon as the design is complete to debug blocks before integration, and to find potential errors long before simulation test environments are available. Questa Formal apps boost productivity and functional verification quality by targeting verification tasks that are difficult to complete.
Questa Formal Verification Apps
See the formal verification apps targeting today’s verification challenges
Questa Inspect
Static RTL Bug Hunting
A fully-automatic formal bug hunting app that finds deeply hidden bugs due to common RTL coding errors, Inspect makes it possible to eliminate a wide range of bugs without a testbench.
Questa Equivalent FPGA
FPGA Equivalence Checking
Questa Equivalent FPGA ensures advanced optimizations needed to meet aggressive power, performance & area goals do not change design functionality, ensuring errors are not introduced …
Questa Verify Property
Exhaustive Verification
Questa Verify Property exhaustively discovers any design errors that can occur, without needing specific stimulus to detect the bug. This ensures that the verified design is bug-free in all legal input scenarios.
Questa Increase Coverage
Code Coverage Closure
Questa Increase Coverage is an automatic formal solution for achieving code coverage closure faster, that addresses an incontrovertible fact of verification: some fraction of uncovered code always remains.
Questa Equivalent RTL
RTL Code Block Comparisons
Questa Equivalent RTL automatically compares specification RTL and implementation RTL code blocks using exhaustive formal analysis. No knowledge of formal or property specification languages is required.
Questa Verify Secure
Secure HW Paths Analysis
The Questa Verify Secure app is a fully automated solution for exhaustively verifying that only the paths you specify can reach security or safety-critical storage elements.
Questa Check Register
Register Verification
The Questa Check Register app automates exhaustive verification of control & status register behaviour against CSV or IP-XACT register specification.
Questa Check Connect
Static & Dynamic Connectivity
The Questa Check Connect app is a fully automated solution for exhaustively verifying static and dynamic connectivity without requiring knowledge of formal or property specification languages.
Questa Check X
X-State Verification
Questa Check X is an automated application that exhaustively roots out ‘X’ issues at the RTL-level without a testbench.
Automatic Push-Button Error Detection
Questa Formal Verification Apps provide easy-to-use automatic checking for many common design errors. With Questa Formal Verification, designers can easily check out new code to look for functional issues such as floating or multiply-driven buses, combinational loops, arithmetic errors and initialisation problems. Finding and fixing these errors before integrating new code into the design avoids injecting difficult-to-find bugs into the larger system, and accelerates downstream verification. Since these checks are based on exact analysis of the reachable state space, the errors detected are real errors, not the noisy results that are often generated by simple lint checkers.
Assertion-Based Formal Verification
Questa Formal Verification also supports general assertion-based formal verification to ensure that the design meets its specific functional requirements. With support for PSL, SVA, and OVL, including multi-clocked assertions, Questa Formal Verification easily verifies even very large designs with many assertions. Its multiple high-capacity formal engines cooperate to complete verification faster. Questa Formal Verification is integrated with the Questa Simulator for easy debug of assertion failures.
Key Features and Benefits
- Each app generates its own assertions, saving hours of work
- Because formal analysis is exhaustive, a formal app tailored to the specific verification task is THE best tool for the job
- High performance formal engines are up to 10x faster than competitive approaches
- No need to wait for simulation or UVM testbench bring-up
- Not limited by time required to simulate all combinations, or by assumptions about what to test for
- Apps take RTL + supporting files as input, generate the required properties, then output waveforms that lead right to the bug
- Results can be integrated with other Questa flows
The Verification Academy
The Verification Academy is a collection of free online courses, focusing on various key aspects of advanced verification.
Tools for Formal Verification
Questa Equivalent FPGA
FPGA Equivalence Checking
Questa Equivalent FPGA ensures advanced optimizations needed to meet aggressive power, performance & area goals do not change design functionality, ensuring errors aren’t introduced …
Questa Formal Verification
Improve Productivity and Assurance
User-friendly automated formal applications simplify the process of identifying and resolving bugs, eliminating the need for specialized formal expertise.
Questa Inspect
Static RTL Bug Hunting
A fully-automatic formal bug hunting app that finds deeply hidden bugs due to common RTL coding errors, Inspect makes it possible to eliminate a wide range of bugs without a testbench.