For a variety of ML applications, generalized matrix multiply (GEMM) with DOT product is the most computationally intensive operation. This paper presents a microarchitecture exploration of fused multi-way reduced precision floating point multiply-accumulate with single rounding, resulting in power and area efficient characteristics. We propose two different microarchitectures, implementing novel design techniques for computing fused FP8 DOT4 accumulating to higher precision FP32 with scaling to adjust the dynamic range. Our first design, dot product with late accumulation, computes fused FP8 DOT4 by calculating the dot product in the first two cycles, expanding the products to fixed point format and another two cycles for the accumulation operation. This design allows the reuse of a slightly modified, FMA capable, FP32 adder. Our second design, dot product with early accumulation is implemented as a standalone FP8 datapath computing products and accumulation in first two cycles, and another two cycles for normalization and single rounding operation. This design aligns addends (products and accumulator) from an “Anchor” for efficient, arithmetically fused, N-way FP DOT product computation. Furthermore, we synthesized the two designs proposed in a 5nm technology node and compared the cost of implementation.

We present a hybrid methodology for the formal verification of arithmetic RTL designs that combines sequential logic equivalence checking with interactive theorem proving in a two-step process. First, an intermediate model of the design is extracted by hand and coded in Restricted Algorithmic C, a simple C subset augmented by the C++ register class templates of Algorithmic C, which provide the bit manipulation features of Verilog. The model is designed to mirror the RTL microarchitecture closely enough to allow efficient equivalence checking, but sufficiently abstract to be amenable to formal analysis. The model is then automatically translated to the logic of the ACL2 theorem prover, which is used to establish correctness with respect to an architectural specification. As an illustration, we describe the modeling and proof of correctness of a chained multiply-add module, designed to test techniques for area and power reduction and intended for implementation in future Arm graphics nrocessors.