Questa Formal Verification
Exhaustive solutions for complex verification challenges
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.