VC Formal 

Next-Generation Formal Verification 

Overview
SoC design complexity demands newer and better verification methods to accelerate verification and debug, as well as reduce overall schedule duration and improve schedule predictability. VC Formal next-generation formal verification has the capacity, speed and flexibility to verify some of the most difficult SoC design challenges, and includes excellent analysis, filtering and debug techniques to quickly identify root causes. In addition, when applied early in the design schedule, before simulation is available, overall schedule improvements can be realized (See Figure 1).

VC Formal Datasheet

VC Formal

Verification Challenges and Modern Formal Verification
The verification of complex chips and systems is a highly challenging task. Techniques to reduce the verification schedule, improve predictability, and accelerate debug are highly desired by engineers and management alike. One way to approach this problem is to move the bug-identification earlier in the cycle as much as possible. When bugs are caught early, they are easier, faster and cheaper to triage, debug and fix. The problem is finding the tougher hard-to-stimulate bugs that result from seemingly impossible-to-think-of corner case scenarios. This is where formal methods come in, as they are less reliant upon the user to think of the potential scenarios that could trigger bugs. When combined with world-class debugging tools and methods, the true power of formal verification is realized.

Formal methods are techniques that can perform analysis on the design independent of, or in conjunction with simulation, and have the power to identify design problems that can otherwise be missed until very late in the project schedule, or even in the manufactured silicon, when changes are expensive and debug is highly challenging and time consuming. When applied early in the design cycle, these methods can identify RTL issues such as functional correctness and completeness well before the simulation test environment is up and running.

VC Formal for next-generation formal verification
Figure 1: VC Formal for next-generation formal verification

Once simulation is available, these methods can combine with simulation to add additional analysis for even better results. Additional techniques can verify SoC connectivity correctness and completeness, isolate differences between two disparate versions of the design, or even between the design and its high-level C/C++ model.

By employing formal techniques at the appropriate time in the design and verification methodology, bugs can be caught significantly earlier in the project, including hard-to-find-bugs that typically elude verification until late in the project. The result is a higher quality design and overall schedule improvements as well as better predictability.

VC Formal
VC Formal is a high capacity, high performance formal verification solution that includes best-in-class algorithms, methodologies, databases and user interfaces. Built from the ground up, this solution was architected to address today’s most challenging verification tasks, and provides the very latest and best formal verification engines available.

Key Features and Benefits

  • Assertion-Based Verification
    Formal proof-based techniques to verify SVA/PSL properties or assertions to ensure correct operation across all possible design activity – even before the simulation environment is available. Advanced assertion visualization and property browsing, grouping and filtering allows simple concise access to results.
  • Advanced Debug
    Advanced debugging interface built on industry standard RTL and waveform visualization solutions, including schematic value annotation for connectivity checking (See Figure 2).

Advanced debug interface
Figure 2: Advanced debug interface

  • Interactivity
    On the fly assertion and constraint editing, incremental build and solve, and proof progress feedback allows instant understanding and control of VC Formal’s activities – without the need to restart (See Figure 3).
  • Interactivity
    Figure 3: Interactivity

  • SoC-level Connectivity Checking
    Verification of connectivity at the full-chip SoC level. Flexible input format ensures ease of flow integration. Powerful debugging, including value annotation, schematic viewing, source code browsing and analysis reporting speeds analysis. Automatic rootcause analysis of unconnected connectivity checks saves significant debug time (See Figure 4).
  • Connectivity checking
    Figure 4: Connectivity checking

  • Sequential Equivalency Checking
    Significantly more powerful next-generation equivalence checking engines that enable comparison of blocks or designs previously too disparate for typical formal comparison. This allows comparison of designs, even after insertion of power gating, or synthesis retiming (See Figure 5).
  • Sequential equivalency checking
    Figure 5: Sequential equivalency checking

  • Certitude Integration
    Certitude™ provides unique information to assess the formal environment. Integrated with VC Formal, Certitude can provide meaningful property coverage measurements within the formal environment as part of the formal IP signoff, and can identify any weaknesses in the formal environment such as missing or incorrect properties or constraints (See Figure 6).
  • Integration with Synopsys’ Certitude functional qualification system
    Figure 6: Integration with Synopsys’ Certitude functional qualification system

  • 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.

Unique Values

  • Industry-leading performance and capacity

    Ability to efficiently run on large designs. At least 5X performance and capacity gains

  • Excellent ease of adoption and ease-of-use

    Use model and commands tightly aligned with Synopsys implementation tools. VC Formal scripts look just like Design Compiler® TCL scripts

  • Run control features

    Enabling grid, pause/resume and save/restore

  • Excellent connectivity checking features, including schematic value annotation and rootcause analysis

    Significantly improving state-ofthe- art debug, including debug of disconnected nets

  • Engine analysis and control

    Ability to examine and control engine activity across the run, and on the fly to better ensure closure on even the most challenging formal problems

Conclusion
Adoption of advanced formal verification techniques is growing rapidly to improve design verification. The automation of certain verification tasks, such as SoC connectivity verification, X-Prop and sequential equivalence checking significantly accelerates the ease of technology adoption. In addition, the common script environment and common setup makes adding launching new formal apps as simple as typing in a few new commands into a previously created script, or a simple click on the GUI. With the integration of industry-standard VCS® simulation and Verdi® debug solutions, the true power of formal verification can be realized.

By employing next-generation formal verification at opportune points in the design verification process, challenging bugs can be caught significantly earlier in the verification schedule, resulting in a higher quality design, overall schedule improvements as well as better predictability.

For more information about Synopsys products, support services or training, visit us on the web at: www.synopsys.com, contact your local sales representative or call 650.584.5000



            NewsArticlesBlogsSuccess StoriesWhite PapersWebinarsVideosTraining Courses