Questa Formal Verification
Complements simulation-based RTL design verification
The Questa® Formal Verification tool complements simulation-based RTL design verification by analyzing all possible behaviors 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 Verification 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. Sharing a common language front end with the Questa Simulator and leveraging the integration with the Unified Coverage Database (UCDB), Questa Formal Verification is the perfect tool to accelerate bug detection, error correction and coverage closure.
How Questa Formal Verification Works
Questa Formal Verification analyzes the behavior of the design to identify all design states that are reachable from the initial state. This analysis allows Questa Formal Verification to explore the whole state space in a breadth-first manner, in contrast to the depth-first approach used in simulation.
Questa Formal Verification is therefore able to discover 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. At the same time, this approach inherently identifies unreachable coverage points, which helps accelerate coverage closure.
Automatic Push-Button Solutions
Questa Formal Verification provides easy-to-use, next generation automatic solutions for checking many common design errors. Questa PropGen and Questa X-Check are the latest technologies added to the Questa Formal-Based portfolio of application-specific tools to address trouble spots in functional verification. Questa PropGen helps verification teams achieve higher quality in complex SoCs by automating the process of assertion-based verification (ABV). The Questa X-Check solution solves the twin problems of X-optimism and X-pessimism that occur due to X-values (unknown signal levels) in designs finding bugs (errors) in the design that would not have been found with traditional verification technology.
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.
We have training courses available for Questa products in our training centers around the world, online, or at your site.