Scholarlink

<p>The popularity of <i>Neural Processing Units (NPUs)</i> is enabled by the growth of Artificial Intelligence. One of the main components of these processors are <i>Multiply and Accumulate (MAC)</i> operations. As these processors are becoming extremely important in the AI era, the design of efficient verification strategies is of utmost importance. In this context, formal verification methods ensure 100% correctness. More specifically <i>Symbolic Computer Algebra</i> (SCA) has been found to be most suitable for multiplier verification. Although there exist many challenges in using SCA-based methods, but the verification process can be performed without the need for a reference model. Therefore, in this paper for verifying MAC operations, we exploit the SCA-based verification method. Experiments are conducted for various MAC designs for bit-width ranging from 8-bit to 128-bit. Various multiplier and adder designs are considered for implementing the MAC. Experiments reveal that certain specific MAC architectures are verification-friendly compared to others.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Formally Verifying Multiply-and-Accumulate Architectures Using Symbolic Computer Algebra

  • 期刊论文

  • 发表日期：

    2026年4月13日

查看全文
  • Lennart Weingarten,
  • Kamalika Datta,
  • Rolf Drechsler

摘要

The popularity of Neural Processing Units (NPUs) is enabled by the growth of Artificial Intelligence. One of the main components of these processors are Multiply and Accumulate (MAC) operations. As these processors are becoming extremely important in the AI era, the design of efficient verification strategies is of utmost importance. In this context, formal verification methods ensure 100% correctness. More specifically Symbolic Computer Algebra (SCA) has been found to be most suitable for multiplier verification. Although there exist many challenges in using SCA-based methods, but the verification process can be performed without the need for a reference model. Therefore, in this paper for verifying MAC operations, we exploit the SCA-based verification method. Experiments are conducted for various MAC designs for bit-width ranging from 8-bit to 128-bit. Various multiplier and adder designs are considered for implementing the MAC. Experiments reveal that certain specific MAC architectures are verification-friendly compared to others.