Formal technologies find obscure bugs and increase design confidence through exhaustive analysis, long before simulation test environments are available. Formal apps boost productivity and functional verification quality by targeting verification tasks that are otherwise difficult to complete.
A broad spectrum of high-powered formal engines, ranging from fully automatic applications such as clock-domain crossing verification, code coverage closure and automatic formal checking to custom-coded assertion property checking, enable non-experts to use formal technology and find bugs early.
Property checking supports assertion-based formal verification to ensure designs meet specific functional requirements, exhaustively discovering any design errors that can occur without needing specific stimulus to detect the bug.
Formal assertion libraries improve quality and reduce schedule times by building protocol and methodology expertise into packages of reusable assertions that support popular industry-standard interfaces.
A fully-automatic formal bug hunting app that finds common RTL coding errors with low effort. Requiring neither a testbench nor assertions, formally verifying designs can start as soon as RTL code is written.
An automatic formal solution for achieving code coverage closure faster. CoverCheck reads code coverage results from simulation via UCDB to target coverage holes.
A fully automated solution for exhaustively verifying static and dynamic connectivity against cleartext CSV. No knowledge of formal or property specification languages is required.
This app leverages formal analysis, as well as property synthesis, to rapidly give you the observability you need to root cause bugs in logic deep within the SoC, and prove fixes don’t break anything else.
A fully automated solution for exhaustively verifying control and status register behavior against a CSV or IP-XACT register specification. No knowledge of formal or property specification languages is required.
A fully automated solution for exhaustively verifying that only the specified paths can reach security or safety-critical storage elements. No knowledge of formal or property specification languages is needed.
SLEC performs exhaustive, formal-based analysis of two RTL inputs in only a few hours or minutes, eliminating manually creating and maintaining testbenches or rerunning massive, time and resource intensive simulation regression.
Questa Formal Verification Apps boost verification efficiency and design quality by exhaustively addressing verification tasks which are difficult to complete with traditional methods, yet don’t require formal or assertion-based verification experience.