- All Products
- Software Integrity
- Semiconductor IP
- Verification
- Design
- Silicon Engineering
- Application Security Services
- Dynamic Analysis (DAST)
- Mobile Application Security
- Penetration Testing
- Managed Static Analysis
- All Services
- Software Security
- Silicon Design
- Community
- About Us
< All Products
< All Products
< All Products
< All Products
< All Products
< All Products
< overview
All Products
+ Software Integrity + Semiconductor IP + Verification + Design + Silicon Engineering + Optical Solutions< Software Integrity
< Software Integrity
Application Security Services
Dynamic Analysis (DAST) Mobile Application Security Penetration Testing Managed Static Analysis< Software Integrity
< Software Integrity
< Software Integrity
Blog
< Software Integrity
Support
< overview
Software Integrity
+ Application Security Products + Application Security Services + Resources + Training & Education Blog Support< Semiconductor IP
< Semiconductor IP
Memories & Libraries
Logic Libraries Memory Compliers Duet Packages HPC Design Kit Embedded Test & Repair Non-Volatile Memory< Semiconductor IP
< Semiconductor IP
Processor Solutions
ARC Processors Embedded Vision Processors Development Tools Operating Systems Ecosystems ASIP Tools< Semiconductor IP
< Semiconductor IP
< Semiconductor IP
< Semiconductor IP
< Semiconductor IP
< overview
< Verification
< Verification
< Verification
< Design
< Design
< Design
< overview
< Silicon Engineering
< overview
< main menu
< Solutions
< Solutions
Industry Solutions
Automotive Cloud Computing Financial Services Industrial Controls Systems Healthcare< Solutions
< overview
< All Services
< All Services
< All Services
< overview
< Software Security
< Software Security
Managed Services
< Software Security
Program Development & Design
Maturity Model (BSIMM) Maturity Action Plan (MAP) Policies & Standards Security Metrics Software Security-in-a-Box< Software Security
< Software Security
Support
< overview
Software Security
+ Software Security Services Managed Services + Program Development & Design + Training Support< Silicon Design
< Silicon Design
< Silicon Design
< Silicon Design
< main menu
< Community
< Community
< Community
< Community
Interoperability
ARC Access HAPS Connect HSPICE Integrator In-Sync System-Level Catalyst TAP-in VC Apps Access< Community
< Community
< Community
< overview
Community
+ Community + SNUG + Partners + Interoperability + Academic Programs + Company Blogs + BSIMM< About Us
< About Us
< About Us
< About Us
< About Us
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 difficult SoC design challenges, and includes comprehensive analysis and debug techniques to quickly identify root causes in the Verdi® debug platform. The VC Formal solution consistently delivers higher performance and capacity, with more 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), Auto Extracted Properties (AEP), Coverage Analyzer (FCA), Connectivity Checking (CC), Sequential Equivalence Checks (SEQ), Register Verification (FRV), Testbench Analyzer (FTA), Formal Navigator (NAV) and a portfolio of Assertion IPs (AIP) for verification of standard bus protocols.
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 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.
- SoC-level Connectivity Checking (CC): Verification of connectivity at the SoC level. 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): This allows comparison of designs, after register retiming, insertion of clock gating for power optimization or microarchitecture changes.
- Formal Navigator (NAV): Enables debug and “what-if-analysis” with only the RTL design in the Unified Verdi GUI with/without assertions or Testbench.
- Register Verification (FRV): Helps to formally verify behavior of configuration registers for respective attributes like “read only”, “read/write” or “reset value” eliminating the need for directed tests.
- Formal Testbench Analyzer with Certitude Integration (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.
- Assertion IP (AIP): High performance and optimized assertion IP for verification of standard bus protocols, and usable in Synopsys VC Formal solution and VCS simulation.
- Advanced Debug and Interactivity: Advanced debugging interface built on Unified Verdi GUI based RTL and waveform visualization solutions, including schematic value annotation, on the fly assertion and constraint editing, proof progress feedback, and cone of influence analysis allows users greater visibility and control.
- Formal Scoreboard: Exhaustively verifies the data integrity of data path designs. Ensures that data is transported through the design without being lost, re-ordered, corrupted or duplicated.
- Formal Coverage: Advanced technologies enable formal metrics and methodology to achieve signoff for property verification.
Event