Formal proof-based techniques to verify SystemVerilog Assertion (SVA) properties to ensure correct operation across all possible design activity even before the simulation environment is available. Advanced assertion visualization, property browsing, grouping and filtering allow simple concise access to results. Formal navigator enables debug and "what-if-analysis" with only the RTL design in the Unified Verdi GUI with/without assertions or Testbench.

Helps formally verify that secure data should not reach non-secure destinations and ensures data integrity, where non-secure data should not over-write (or reach) secure destinations.

Provides significant performance improvement to formal property verification using Machine Learning technology. Use of this app accelerates formal property verification to achieve better convergence of formal proofs for subsequent runs and enables significant saving of compute resources in nightly formal regressions.

Testbench Quality Assurance provides the unique capability to assess the quality of formal environment. The native integration of Testbench Quality Assurance with VC Formal provides meaningful property coverage measurements as part of formal signoff and identifies any weaknesses such as missing or incorrect properties or constraints. The native integration delivers 5-10X faster performance compared to stand-alone fault injection methods.

Integrated HECTOR™ technology within VC Formal and contains custom optimizations and engines for datapath verification (ALU, FPU, DSP etc.) using transaction level equivalence. This app leverages the Verdi graphical user interface for debug.

Functional safety verification is an essential requirement for automotive SoC and IP designs. This App formally identifies and classifies faults based on observability or detectability criteria. Complementing fault simulation with Z01X™, the combined solution reduces the effort and time required to achieve the test coverage closure and meet functional safety objectives.