A Case Study on Formally Verifying an Open-source Deep Learning Accelerator Design

Deep learning accelerators play a crucial role in accelerating the performance of deep neural networks. As these accelerators become more complex, ensuring their correctness and reliability becomes increasingly challenging. Formal verification techniques offer a systematic approach to rigorously validate the design and verify its functional correctness. In this case study, we present a detailed analysis of verifying an open-source deep learning accelerator design (at RTL abstraction), highlighting the methodology, challenges, steps and outcomes of an enhanced formal verification process.