1124: Achieving End-to-End Formal Verification of Large Floating-Point Dot Product Accumulate Systolic Units

Dot Product Accumulate Systolic units are a primary part in the ML accelerator architectures. They compute floating-point matrix multiply-add operations, which consist of several dot products. Given that exhaustive simulation is impossible in real use cases, Formal Verification is the only possible option to verify these components. C2RTL Formal Equivalence Checking has shown to be a very powerful methodology, and to deploy it successfully an independent, trust C/C++ reference model is required. In this paper, we present a comprehensive End-to-End (E2E) Formal Verification Signoff approach for DPAS units. The proposed flow begins with a new formal friendly C++ model, created using an internal iFP library, developed starting from the FPCore functional programming language, and validated against 3rd party trusted libraries. Then the flow continues with a C2RTL equivalence checking to establish the RTL correctness, where the assumptions used are encoded in the RTL itself as SVA properties and tested using simulation and formal property verification. Several hard corner-case bugs have been identified in intermediate versions of the RTL with this methodology. Innovative techniques have been developed to achieve full convergence, in particular for large double precision units, proving that the final RTL doesn’t have any bug against the reference model.