AI And ML Applications Require Advanced Datapath Verification

In popular usage, the term “artificial intelligence” (AI) once conjured up images of robot armies subjugating humans or evil computers outsmarting their users, as in ‘2001: A Space Odyssey.’ In recent years, AI has become a part of daily life for much of the planet’s population. People use voice commands to interact with their smartphones, smart speakers and even TV remote controls. Sophisticated image processing is behind countless sensors and at the heart of many security applications. Autonomous vehicles rely on a range of AI technologies to understand their environment and make driving decisions. Even non-autonomous vehicles have smart features such adaptive speed control and lane departure warning systems.

Behind the scenes, AI-based devices use machine learning (ML) and deep learning (DL) to improve their recognition and decision-making capabilities over time. These powerful technologies do not come cheap. They require a rich combination of hardware and software within highly sophisticated embedded systems. There is a great deal of mathematics involved in AI. This includes all the traditional arithmetic and logical functions, floating-point operations, and digital signal processing (DSP) algorithms. These are extended by newer techniques ideal for natural language and image processing, including convolutional neural networks (CNNs). The speed required to make decisions and react to real-world conditions means that key portions of AI-related computations must be done in hardware.

The current generation of chips for AI/ML/DL applications contain complex datapaths to perform the required mathematical analysis. For example, Maxim recently announced its MAX78000 system-on-chip (SoC), containing a CNN accelerator with 64 parallel processors and capable of 30 billion operations per second. Alibaba’s AI inference chip, Hanguang 800, can process nearly 80 thousand images per second. Google’s Tensor Processing Unit (TPU) machine learning chip now powers many of its most popular features, including text and image searches, language translation, and voice recognition. There are numerous other examples available in the industry today. For companies wishing to develop their own AI chips, companies like Synopsys offer powerful IP building blocks such as the DesignWare Library Datapath IP.

Given the importance of mathematical operations in AI applications and the complex datapaths required to perform these operations, thorough verification is critical. Simple math shows that exhaustive exercise of all possible data values is impossible in simulation, emulation, or even hardware prototypes. Consider just one multiplier with two 32-bit inputs, which has 2⁶⁴ possible input combinations. Even if the verification process can execute and check one million multiplications per second, it would take nearly 600 thousand CPU-years to cover all values. That’s just for one multiplier; AI datapaths have many arithmetic elements running in parallel. Clearly, a better approach is needed.

When exhaustive verification is desired, but an iterative approach is impractical, formal methods should be considered. Formal verification uses mathematical analysis to consider the entire hardware design at one time. The traditional form of formal verification is model checking, in which the design is verified against a set of assertions specifying the intended behavior. The analysis tries to either provide that the design satisfies the assertions or generate counterexamples for any mismatches. This approach works very well on control logic and even small datapath elements. However, the sheer size and complexity of an AI IP or chip means that it cannot be fully proven by model checking.

The other main form of formal verification is equivalence checking, in which two representations of the design are compared. The analysis tries to either prove equivalence or show where the designs differ. Equivalence checking is commonly used to check the register transfer level (RTL) input against the gate-level netlist produced by logic synthesis. If the state elements (memories and flip-flops) are identical in the two representations, then the comparison involves only combinational logic and is relatively straightforward. If the state elements differ, for example if the synthesis process moves logic across register boundaries, then sequential equivalence checking is required. This technique compares the outputs of the two design representations regardless of the number of state elements in each.

Equivalence checking provides a powerful method for verifying the most complex AI datapaths. With sufficient powerful formal engines, the two representations can be at vastly different levels of abstraction, and even written in different languages. For example, the detailed RTL implementation can be compared to a high-level C/C++ architectural model. The inner details are irrelevant; the comparison confirms that the same set of inputs produces the same outputs for both representations. This approach is a natural fit for many AI projects since they already have C/C++ models available for results checking in simulation or as part of a virtual platform to support early software development and test.

The Synopsys VC Formal Datapath Validation (DPV) App using HECTOR technology is a transactional equivalence checker with the power to verify complex AI datapaths, including DSP engines, floating-point units (FPUs), graphics processing units (GPUs) and CNNs. It reports any differences in the results of the RTL and C/C++ models for diagnosis in the Synopsys Verdi SoC debug platform and proves equivalence once all differences have been resolved. The DPV App has been used successfully by many leading-edge chip development teams. Engineers from Samsung, Intel, AMD, NVIDIA, Qualcomm, Imagination Technologies, and emerging AI/ML chip companies have used the DPV App and presented conference papers summarizing their experience and results.

Equivalence checking flow for AI datapaths

Today’s AI/ML/DL designs are math-intensive, with complex datapaths packed with powerful arithmetic engines. The criticality of the applications supported requires fully verified designs; no one wants their self-driving car to collide with an obstacle missed by the image recognition analysis. Formal equivalence checking is the only technology that can provide exhaustive verification of datapath designs against a proven reference model. The Synopsys VC Formal DPV App has a long history of successful deployment for the most demanding AI chip projects. The Synopsys DesignWare ARC EV Processors for Embedded Vision are also verified using this technology. More information on users and more technical details about the Synopsys flow can be found in an earlier blog post. A webinar with a demonstration of the verification flow is also available.