VC Formal

Next-Generation Formal Verification

SoC design complexity demands fast and comprehensive verification methods to accelerate verification and debug, as well as shorten overall schedule and improve predictability. The VC Formal™ next-generation formal verification solution has the capacity, speed and flexibility to verify some of the most complex SoC designs and includes comprehensive analysis and debug techniques to quickly identify root causes leveraging Verdi® debug platform. The VC Formal solution consistently delivers highest performance and capacity, with more design bugs found, more proofs on larger designs and achieves faster coverage closure through the native integration with VCS® functional verification solution.

The VC Formal solution includes a comprehensive set of formal applications (Apps), including Property Verification (FPV), Automatic Extracted Properties (AEP), Coverage Analyzer (FCA), Connectivity Checking (CC), Sequential Equivalence Checking (SEQ), Register Verification (FRV), X-Propagation Verification (FXP), Testbench Analyzer (FTA), Regression Mode Accelerator (RMA), Datapath Validation (DPV) and a portfolio of Assertion IPs (AIP) for verification of standard bus protocols.

Download Datasheet

Productivity Apps

Features and benefits of VC Formal's formal verification techniques

High Value Apps

Features and Benefits:

Assertion-Based Property Verification (FPV): 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 allows simple concise access to results.
Automatic Extracted Property Checks (AEP): Automatic functional analysis for out of bound arrays, arithmetic overflow, X-assignments, simultaneous set/reset, full case, parallel case, multi driver/conflicting bus and floating bus checks without the need for dedicated simulation tests.
Formal Coverage Analysis (FCA): Complementing simulation flows, VC formal provides proof that uncovered points in coverage goals are indeed unreachable, allowing them to be removed from further analysis—saving significant manual effort.
Connectivity Checking (CC): Verification of connectivity at the subsystem or SoC levels. Flexible input format ensures ease of integration. Powerful debugging, including value annotation, schematic viewing, source code browsing and analysis reporting speeds analysis. Automatic root-cause analysis of unconnected connectivity checks saves significant debug time.
Sequential Equivalency Checking (SEQ): Verify modifications to the designs that do not affect the output functionality. For example, changes after register retiming, insertion of clock gating for power optimization or microarchitecture changes can be exhaustively verified without running any simulations.
Register Verification (FRV): Formally verify that the attributes and behaviors of configuration and status register addresses and fields are correctly implemented and accessed. For example, attributes such as “read only”, “read/write” or “reset value” can be defined in IP-XACT and formally verified, eliminating the need for directed simulation tests.
X-Propagation Verification (FXP): Checks for unknown signal value (X) propagation through the design and allows tracing of the failed property to source of X in the Verdi schematic and waveform.
Formal Testbench Analyzer (FTA): Certitude™ provides the unique capability to assess the quality of formal environment. The native integration of Certitude 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.
Security Verification (FSV): 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.
Datapath Validation (DPV): 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.
Regression Mode Accelerator (RMA): 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.
Assertion IP (AIP): A portfolio of high performance and optimized Assertion IPs for standard bus protocols are available for all VC Formal Apps as well as VCS and ZeBu®. Some of the most popular titles available are Arm® AMBA® APB, AHB, AXI3, AXI4, ACE-lite, ACE, and CHI protocols.