The IBM z Systems(TM) is the backbone of the insurance, banking, and retail industry. Innovation in these markets is driving the demand for new and additional applications to better serve the customers. These workloads like machine learning, data analytics, AI, etc. require a rapidly increasing number of computations in smaller precision formats. With IBM z15(TM) we completely redesigned the binary and hexadecimal floating-point unit to efficiently implement SIMD operations at 5.2GHz while maintaining the industry leading reliability, availability and serviceability standard. This paper describes the new design and special techniques used to achieve these goals like reusing the existing double precision unit pipeline for lower precision parallel SIMD, new approaches to formally verify the design, and improving error detection for the 14nm technology node.

Advances in deep neural networks (DNNs) and the availability of massive real-world data have enabled superhuman levels of accuracy on many AI tasks and ushered the explosive growth of AI workloads across the spectrum of computing devices. However, their superior accuracy comes at a high computational cost, which necessitates approaches beyond traditional computing paradigms to improve their operational efficiency. Leveraging the application-level insight of error resilience, we demonstrate how approximate computing (AxC) can significantly boost the efficiency of AI platforms and play a pivotal role in the broader adoption of AI-based applications and services. To this end, we present RaPiD, a multi-tera operations per second (TOPS) AI hardware accelerator core (fabricated at 14-nm technology) that we built from the ground-up using AxC techniques across the stack including algorithms, architecture, programmability, and hardware. We highlight the workload-guided systematic explorations of AxC techniques for AI, including custom number representations, quantization/pruning methodologies, mixed-precision architecture design, instruction sets, and compiler technologies with quality programmability, employed in the RaPiD accelerator.

The combination of growth in compute capabilities and availability of large datasets has led to a re-birth of deep learning. Deep Neural Networks (DNNs) have become state-of-the-art in a variety of machine learning tasks spanning domains across vision, speech, and machine translation. Deep Learning (DL) achieves high accuracy in these tasks at the expense of 100s of ExaOps of computation; posing significant challenges to efficient large-scale deployment in both resource-constrained environments and data centers.

Floating Point Units (FPUs) pose a singular challenge for traditional verification methods, such as coverage driven simulation, given the large and complex data paths and intricate control structures which renders those methods incomplete and error prone. Formal verification (FV) has been successfully leveraged to achieve the high level of quality desired of these critical logics. Typically, FV-based approaches to verify FPUs rely on introducing higher level abstractions to allow reasoning. This however has to be done manually, and quickly becomes tedious for optimized bit level implementations on board high performance microprocessors. Automated formal methods working directly on the bit level and providing a full end-to-end check exist but are limited to single instructions (issued in an empty pipeline), hence lack in checking control aspects related to inter-instruction interactions, or pipeline control. In this paper we present an approach based on equivalence checking to overcome the single instruction limitation for automated bit level proofs in the formal verification of FPUs. The sequential execution of instructions is modeled by two instances of the design-under-test. One of the instances acts as a reference model for the other. This allows for large numbers of internal equivalences to be leveraged by equivalence checking techniques. We show that this method is capable of proving instruction sequences for industrial FPU designs. Together with a proof of correctness of individual instructions it guarantees correctness of the FPU design as a whole. In our experience this is a one of a kind approach to perform automated end-to-end verification of FPUs.