Synopsys Cloud
Cloud native EDA tools & pre-optimized hardware platforms
Request a Free Trial →
Table of Contents
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. Virtual Conference. In the meantime here’s a primer on datapath validation and HECTOR technology to get you up to speed. Read on.
Q: What is datapath validation and why is it important?
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.
Q: What is HECTOR technology and why is it useful for datapath validation?
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.
Q: How does HECTOR technology help simplify the difficult task of datapath validation?
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:
- Fast and efficient formal algorithms, including multiple solvers for tackling complex mathematical logic
- Rapid convergence technology, including automatic design partitioning and multi-processor support
- Advanced debug support, including an integrated debugger that allows single stepping of C/C++ code
- And flexible language support: Verilog, VHDL, SystemVerilog, C, C++14/17
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: Example Image Description
Q: What are the biggest challenges of equivalence checking and how does HECTOR technology overcome them?
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.
Q: What are the origins of HECTOR technology?
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).
Q: How has HECTOR technology transitioned from primarily serving CPU and GPU companies to more AI chipmakers?
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.
Q: How does Synopsys ensure that its own floating-point components are bug-free?
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.