Synopsys Delivers 100X Faster Formal Verification Closure for AI, Graphics, and Processor Designs

Reading Time: 2 minutes


  • VC Formal Datapath Validation application delivers over 100X speed-up in formal verification between a reference C/C++ algorithm and RTL design implementation over conventional techniques
  • The new app integrates VC Formal’s debug and usability features enabled through Verdi with proven HECTOR technology

Synopsys, Inc. (Nasdaq: SNPS) today introduced the Datapath Validation (DPV) app as part of its VC Formal® solution. The DPV app leverages proven HECTOR™ technology to deliver exhaustive formal verification closure on datapath-intensive designs during the design and verification cycle for broad market adoption. The app also delivers over 100X speed-up in formal verification between a reference C/C++ algorithm and RTL design implementation over conventional techniques of complex system-on-chip (SoC) designs, and enables exhaustive functional verification in situations previously deemed impractical.

“Our mission is to develop high-quality CPU, GPU, and system IP for mobile SoC applications, which requires a highly competitive feature set, excellent overall performance, and very low power consumption under extremely tight schedules,” said Xiushan Feng, Formal Verification Lead for the GPU & CPU team at Samsung SARC and Advanced Computing Lab. “Formal verification of C/C++ algorithms provides exhaustive verification for our datapath-centric designs to efficiently discover corner-base bugs in minutes, where other techniques would have been impractical. VC Formal’s HECTOR technology delivers best-in-class performance and quality of results, which enabled us to successfully reduce our simulation efforts and helped catch more than 30 RTL bugs in our designs.”

Artificial intelligence (AI), graphics, and processor designs involve complex algorithmic functional blocks that are datapath heavy and require their behavior to be modeled in high-level languages such as C/C++. The implemented RTL for these designs needs to be subsequently verified for functional equivalence with the C/C++ model. The native integration of VC Formal with Synopsys’ Verdi® automated debug system enables design and verification teams to easily leverage formal technologies and automate root cause analysis of formal results. Additionally, the native integration of VCS in VC Formal facilitates easy insertion of formal analysis into the existing verification environment.

The DPV app joins the growing portfolio of VC Formal apps, including Property Verification (FPV), Sequential Equivalence Checks (SEQ), Register Verification (FRV), Formal Coverage Analyzer (FCA), Connectivity Checking (CC), X-Propogation Checks (FXP), Formal Testbench Analyzer (FTA), Automatic Extraction of Properties (AEP), and Regression Mode Accelerator (RMA).

“There is an increase in datapath-intensive designs that require specialized datapath validation techniques to achieve faster verification closure,” said Ajay Singh, senior vice president of Engineering in the Verification Group at Synopsys. “We have long collaborated with industry leaders to deliver comprehensive verification solutions for advanced SoCs. Our investment in datapath validation technology enables a faster path to verification closure and accelerate time-to-market.”


SOURCE Synopsys, Inc.