By Pratik Mahajan, R&D Group Director; Alfred Koelbl, Synopsys Scientist; and Kiran Vittal, Sr. Product Marketing Director; Verification Group
From portable speakers to factory equipment, medical devices, and cars, the things in our lives are becoming increasingly intelligent. It’s no wonder that designing chips for artificial intelligence (AI) and machine-learning (ML) applications is becoming a big business, with new startups to larger, established companies getting into the game. AI/ML as well as CPU/GPU designs involve a lot of arithmetic computation with datapath logic, including all the traditional arithmetic and logical functions, floating-point operations, and digital signal processing (DSP) algorithms. Datapath validation is essential in ensuring that your design will be bug-free and be able to pass stringent tape-out criteria. One of the most effective and efficient technologies for exhaustive verification of complex datapath designs is HECTOR™ technology.
You can learn more about HECTOR technology from our sessions at the DVCon U.S. 2021 and DVCon U.S. 2022 Virtual Conference. In the meantime here’s a primer on datapath validation and HECTOR technology to get you up to speed. Read on.
A: Chips that use floating-point arithmetic, such as CPUs, GPUs, and AI hardware, process millions of highly precise calculations. They require complex datapaths to perform this mathematical analysis. However, corner-case bugs in the datapath can go undetected and, thus, lead to system failures. Calculating the trajectory of a rocket, for example, needs to be very precise. A subtle bug in a floating-point unit (FPU) could potentially cause the rocket to crash. The process of datapath validation identifies those bugs.
Traditional verification methods based on simulation, for instance, are inefficient, time-consuming, and simply impractical for exhaustively verifying these complex mathematical functions. Formal verification—which uses mathematical methods to prove or disprove the correctness of intended algorithms—provides an effective, efficient, and tractable solution.
A: HECTOR stands for High-level Equivalence C++ to RTL and is available in the Synopsys VC Formal® Datapath Validation (DPV) App, which is part of the VC Formal product family. Most commercially available formal verification tools focus exclusively on verification of control logic. VC Formal DPV with integrated HECTOR technology is the only commercially available formal verification tool for exhaustive verification of datapath elements, using formal solvers on the data transformation areas of the design. The technology contains custom engines for datapath validation covering arithmetic logic unit (ALU), FPU, and DSP blocks.
A: HECTOR technology provides equivalence checking of independently developed models. It exhaustively verifies that an RTL implementation is equivalent to a trusted C/C++ reference model. It can also be used to exhaustively verify successive design refinements, from C to C, C to RTL, and RTL to RTL, without requiring any testbenches, assertions, or coverage (Figure 1). And it’s great for detecting corner-case bugs. The technology is built with:
HECTOR delivers 100% confidence that the RTL design implementation conforms to the C/C++ reference algorithm, thereby significantly speeding up signoff for datapath components as compared to simulation-based techniques.
Figure 1: VC Formal DPV with HECTOR technology exhaustively verifies successive design refinements without requiring testbenches.
A: For many designers, creating the reference model itself is one of the biggest challenges of equivalence checking. Many companies have already adopted a design flow that starts with a trusted C++ reference model. Even if such a design flow is not in place, Synopsys provides a comprehensive, formally verified C++ math library that customers can use to verify their RTL. Alternatively, customers can download open-source libraries, which, for example, exist for many floating-point algorithms and for encryption/decryption algorithms.
A: A team of Synopsys engineers (part of the Advanced Technology Group) whose charter was to develop advanced new technologies and ideas created HECTOR technology. Up until then, floating-point bugs had triggered some very costly, attention-grabbing losses, from a rocket launcher that exploded after nearly 40 seconds in flight to a radiation therapy machine that caused death and injury due to improper dosage calculations, as well as some more infamous incidents. These episodes provided motivation for the team.
Recognizing that design architects liked to write their specifications in form of C or C++ reference models, the team explored whether they could develop verification technology that would determine whether the RTL created by hardware designers would be equivalent to the C/C++ models.
When the power of HECTOR technology became obvious, the team matured the tool by working on customer designs from a variety of domains, including GPUs, CPUs, networking, and security. That early HECTOR technology (so named in the interest of having a short, catchy moniker) has evolved to become VC Formal DPV, which now supports all modern C++ languages and a complete debug environment based on the industry-leading Synopsys Verdi® SoC Debug Platform (Figure 2).
Figure 2: VC Formal DPV with HECTOR technology supports all modern C++ languages and a complete debug environment.
A: When Synopsys started the datapath validation journey back in 2002, AI was not on anyone’s radar. Synopsys mostly focused on graphics companies, as their applications are compute-intensive. In the last five to six years, more and more companies, especially new AI startups, have emerged and begun using HECTOR technology to verify their datapaths. The compute part of an AI chip requires a lot of floating-point operations, so HECTOR is a good fit. AI chipmakers can often afford to sacrifice precision for computation speed, so they may have floating-point computations at 16 bits or less. That yields 100% datapath validation right out of the box with VC Formal DPV. To accommodate AI chips, we’ve also continued to expand our math library. We’ve been doing floating-point verification for so many years and are continuing to build on our expertise.
A: We’ve verified all of our DesignWare® processor solutions that contain arithmetic floating-point components with HECTOR technology. We’ve made this technology easy to use; most of the top CPU, GPU, and processor companies are using our technology, and we’re taking advantage of it, too.
We look forward to seeing you at this year’s virtual DVCon to share more details about how HECTOR technology can help you solve your datapath validation challenges. See you online!
Catch up on some of our other recent AI-related blog posts:
Also, be sure to sign up for and watch our on-demand webinar, “Faster Formal Verification Closure for Datapath in AI & Processor Designs.” Neelabja Dutta, one of our applications engineers, will share techniques to achieve faster convergence.