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 tool complements 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 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 Questa Advanced 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.



Questa Formal Verification Apps Workflow






Questa Formal Verification Apps

See the formal verification apps targeting today’s verification challenges


Questa AutoCheck


A fully-automatic formal bug hunting app that finds bugs due to common RTL coding errors, AutoCheck makes it possible to eliminate a wide range of bugs with low effort.


More Info

Questa CoverCheck


Questa CoverCheck 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.

More Info

Questa Property Checking


PropCheck 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.

More Info

Questa Register Check


Questa Register Check app automates exhaustive verification of control&status register behavior against CSV or IP-XACT register specification.


More Info

Questa Connectivity Check

The Questa Connectivity Check app is a fully automated solution for exhaustively verifying static and dynamic connectivity without requiring knowledge of formal or property specification languages.

More Info

Questa SLEC


Questa SLEC automatically compares specification RTL and implementation RTL code blocks using exhaustive formal analysis. No knowledge of formal or property specification languages is required.

More Info

Questa Formal Assertion Library

A Formal Assertion Library improves quality and reduces schedules by building protocol and methodology expertise into packages of reusable assertions that support popular industry-standard interfaces.

More Info

Questa Secure Check


The Questa Secure Check app is a fully automated solution for exhaustively verifying that only the paths you specify can reach security or safety-critical storage elements.


More Info

Questa X-Check


Questa X-Check is an automated application that uses formal algorithms under-the-hood to exhaustively root out ‘X’ issues; but you don’t need to know Formal to use it.

More Info





How Questa Formal Verification Works

Questa Formal Verification analyses the behaviour 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 Error Detection

Questa Formal Verification provides 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.