Next-Gen Static & Formal Technology for Verification Compiler

VC Formal provides state-of-the-art property checking as well as sequential equivalence checking, connectivity checking and formal coverage analysis. VC CDC provides clock domain crossing verification that is uniquely capable of checking entire SoCs at RTL. VC LP provides low power verification of the most advanced designs based on the Unified Power Format (UPF). The next-generation database and engines offer 3X to 5X performance and capacity compared to previous generation products.

"Aquantia is the market leader in high-speed Ethernet connectivity solutions for cloud computing, data centers and enterprise infrastructure. Low power design is crucial for our award-winning 28 nanometer 10GBASE-T products," said Darren Engelkemier, vice president of digital IC engineering at Aquantia. "Aquantia was one of the first users of Synopsys' next-generation low power static checking technology. VC LP's performance, capacity and ease-of-use simplified our complex low power verification and debug."
"As SoC complexity grows, design and verification teams are increasingly turning to several static and formal verification technologies to expand their verification capabilities. Historically, these teams have been challenged with use-model, debug, performance and capacity limitations," said Prosenjit Chatterjee, GM of North America at Oski Technology. "With VC Formal, VC LP, and VC CDC Synopsys offers a unique approach to combine all these solutions on a single, high-performance, high-capacity data model, with new analysis and debug engines to address many of these traditional challenges."  

Synopsys' next-generation static and formal technology is built on a fundamentally new approach—it's architected to broadly support and unify formal techniques, static analysis, simulation and other verification technologies. This unique level of integration and interoperability allows formal verification to work in concert with the other tools and technologies to find bugs faster and more accurately, reduce spurious results and accelerate root- cause determination. In addition, this technology supports new formal/simulation coverage metrics that improve the predictability of verification closure.

Synopsys' next-generation static technology takes full advantage of the incredible capacity and performance offered by new data models and databases to enable checking entire SoCs at RTL flat, allowing these new products to find bugs that previous tools and technologies can't. As an example, deep CDC reconvergence bugs only manifest when the entire SoC is analyzed, which requires enormous capacity. In addition, this technology provides users great flexibility in specifying any type of clock domain crossing synchronizer structure and offers unprecedented power in analyzing these structures for defects or incompleteness. Synopsys' next-generation static and formal technology also leverages common and familiar Design Compiler and IC Compiler use models, greatly shortening the learning curve and flow integration effort associated with previous generation technologies. As a result, users are able to leverage existing Design Compiler and IC Compiler setup scripts to quickly get started with low power and CDC static verification.

"We have been collaborating closely with many customers on our next-generation static and formal verification technologies, which are essential to effectively address the increasing verification challenges of complex SoCs," said Manoj Gandhi, senior vice president and general manager of the Synopsys Verification Group. "We have made a significant investment during the past few years in these leading-edge technologies, which are key elements in Verification Compiler, in order to provide designers with superior static and formal solutions already proven in several successful designs."