Questa Formal Verification

Even the most carefully designed testbench is inherently incomplete since constrained-random methods cannot hit every corner case. Unfortunately, even after 100% functional coverage is achieved there can still be showstopper bugs hiding in unimagined state spaces. Questa® Formal Apps statically analyze a design’s behavior with respect to a given set of properties; then exhaustively explore all possible input sequences in a breadth-first search manner. This uncovers design errors that would otherwise be missed or are impractical to find with simulation-based methods.

Automated formal applications

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.

Properties are synthesized from a combination of automatic RTL design analysis and a high-level specification of design intent. The generated properties are then exhaustively verified with formal analysis engines.

The Questa Formal App suite includes applications to address tasks such as: static and conditional connectivity checking, secure path integrity checking, unreachable code identification, X-state propagation, state-space analysis, and register verification. Additionally, the Questa Sequential Logic Equivalence Checking (SLEC) App uses formal methods to perform exhaustive comparisons between inputs to reveal any behavioral discrepancies that could arise in clock gating, ECO integration, re-pipelining, or fault mitigation logic.