Synopsys Cloud
Cloud native EDA tools & pre-optimized hardware platforms
Request a Free Trial →
In electronic design, bugs are inevitable. As chips continue to grow larger and more complex, the impact of these trouble spots will only become more devastating. Fortunately, the chip verification toolbox keeps evolving as well, providing you with ways to catch bugs early in the chip design cycle, before they are costlier to address.
Formal verification uses mathematics—static analysis algorithms in particular—to prove chip design correctness. Complementing traditional simulation methods, formal verification provides a much more exhaustive means to uncover the hard-to-find corner-case bugs that elude simulation. Verification engineers using the methodology can find more bugs faster, often before the simulation testbench is ready. Engineers can complete signoff on blocks with a formal specification (high-level behavior or properties) and their implementation (design RTL).
While the process has become more mainstream, and there are many formal apps that are easy-to-use and don’t require formal expertise, formal property verification (FPV) is still considered a specialized skill in the verification world. As a result, it takes time and effort to become productive with the methodology. This is where experts can step in to help verification teams accelerate their adoption of formal technologies and, once that is done, become more productive using these products to achieve faster coverage closure.
In this blog post, I’ll discuss how Synopsys Formal Verification Services can help your team maximize the value of formal verification. Read on to learn about the difficult verification challenges our seasoned experts can help you solve with our deep expertise and variety of service options.
What Makes Formal Verification Challenging?
When formal verification was introduced a few decades ago, the perception was that a Ph.D. in the subject was needed to use the methodology. SystemVerilog, the hardware description and verification language used in modeling, designing, simulating, testing, and implementing electronic systems, was not commonly known at the time. In the early 2000s, many formal startups had their own property languages and there was little compatibility between tools. Over the years, consolidation took hold, and more engineers began writing SystemVerilog assertions. Today, the SystemVerilog language is an industry standard, well-known by chip verification engineers now accustomed to writing assertions and developing formal testbenches. Without formal verification, it would be nearly impossible to find all corner-case bugs. The human brain is simply not wired to come up with the seemingly endless input combinations to exhaustively verify each block of each design.
Formal verification can exhaustively verify a block using mathematical proof without the need of enumerating all input combinations. However, it does take effort to write assertions that can be verified with FPV to provide conclusive results on whether the assertions pass or fail the design, and when some of the assertions fail to debug the assertion failure. Another possible outcome of FPV is inconclusive results where FPV tools are not able to conclusively prove or falsify the assertions under the time and resource constraints. Often techniques such as writing abstraction models are needed to reach convergence. Even though designers have deep knowledge of the blocks and designs they’re verifying, for many, writing abstraction models to address inconclusive findings is not easy.
Synopsys VC Formal™ next-generation formal verification solution provides the capacity, speed, and flexibility to verify complex SoCs. Machine learning techniques have been used in the VC Formal solution to improve performance and reduce the user debugging effort. For example, Smart Strategy Selection enables smart engine orchestration by learning, during the run, to assign the best engine to the assertions to be verified, leveraging the right resources. Regression Mode Accelerator (RMA) allows learning to continue in subsequent regression runs to optimize performance and improve convergence. Machine learning is also used in debugging. When there are many violations, some are bound to be caused by the same issues. VC Formal technology clusters violations based on root-cause analysis so that when one is fixed, the others are also fixed, reducing user debugging effort.
Expert Formal Verification Pros Around the World
To help customers quickly ramp up their productivity with the VC Formal technology, Synopsys Formal Verification Services provide assistance, ranging from methodology training to verification audit to turnkey projects. Experts are located across the globe; engagements last anywhere from a week up to 16 weeks or more. Our team has experience solving an array of complex problems:
- Advanced formal property verification and signoff
- Architectural formal model development and validation
- Assertion IP development for proprietary and customer protocols
- Datapath validation
- Security verification
- Functional safety
- Apps deployment
Options for our consulting services, which feature training labs and materials as needed, include:
- Formal Verification CoStart, which helps customers get started via set up of the methodology, flow, and script, providing new users a general understanding of how to use the tool. Without a statement of work (SOW) requirement, the CoStart service provides the flexibility for customers to prioritize the activities they’d like to have covered.
- Bootcamp-style training, which covers formal methodology, coding, and optimizing for formal, writing advanced checkers and scoreboards, constraints and over-constraining, and convergence.
- Assessment with formal audit, which provides a review of existing formal flows, usage, and methodologies, along with recommendations for appropriate metrics for signoff and closure.
- Hand-in-hand/joint project consulting, which provides training, auditing, and help with test plan creation. Synopsys consultants maintain partial ownership of the project, working closely with the customer to help them be productive with the tool.
- Turnkey project consulting, where Synopsys consultants take full ownership of the project, delivering the final setup, SystemVerilog assertions, results, documentation, and knowledge transfer.
Case Studies: Uncovering Corner-Case Bugs
As an example of the impact these services can make, consider a case study involving data path validation in a DSP block using the VC Formal DPV App. This block contained 30 multipliers as well as fixed-to-floating conversion units and floating-point arithmetic logic units. Our team developed the formal test plan, assumptions to model the pre-loading sequence, and assumptions on a large number of input signals at the top level, achieving conclusive formal proofs on the module and top level. Among the results: seven corner-case bugs discovered across the reference model and implementation RTL, as well as documentation, methodology knowledge transfer, and verification setup for future use.
Another case study involves a direct memory access (DMA) broadcast block featuring multiple reused blocks and both standard and proprietary interfaces. Our team developed the formal verification test plan, wrote assertions and environment assumptions, and leveraged AXI assertion IPs (AIPs) for interface target assertions and constraints. The team also provided formal signoff with high coverage numbers (88% to 95%) using advanced formal metrics and faults injected through the Formal Testbench Analyzer (FTA) App. Among the results: discovery of multiple RTL and specification bugs with two critical corner-case bugs in previously verified blocks, plus delivery of formal signoff metrics and setup for future use.
Summary
While it takes effort to write assertions and debug failures, formal verification is an essential component of a verification process, given its adeptness in finding corner-case bugs. The Synopsys VC Formal solution provides a comprehensive array of formal apps to support the process, delivering the capacity, speed, and flexibility to verify complex SoCs. To help customers accelerate their implementation as well as their productivity with the VC Formal solution and formal verification techniques, Synopsys Formal Verification Services provides a team of worldwide experts. With a helping hand from our consultants, customers can benefit from knowledge transfer, an efficient path toward formal verification productivity, faster coverage closure, and, ultimately, formal signoff.