一种以高密度脂蛋白（HDL）为核心的合成与验证方法，用于基于随机存取存储器（RRAM）的神经形态系统

《Microprocessors and Microsystems》：An HDL-centric synthesis and verification approach for RRAM-based neuromorphic systems

　　法特梅赫·希林扎德（Fatemeh Shirinzadeh）| 卡玛莉卡·达塔（Kamalika Datta）| 阿博伊·科莱（Abhoy Kole）| 萨伊德·希林扎德（Saeideh Shirinzadeh）| 罗尔夫·德雷克斯勒（Rolf Drechsler）
德国不来梅大学

**摘要**
电阻式随机存取存储器（RRAM）通过结合存储和计算功能实现了内存计算，并支持多种内置操作，包括由交叉架构自然支持的“乘法与累加”（MAC）操作。尽管MAC在神经形态系统中得到了广泛应用，但其用于通用布尔逻辑的应用仍然处于探索阶段。本文提出了一种基于RRAM交叉架构的逻辑计算（LiM）系统的综合与验证方法，该方法具有更高的抽象层次。我们引入了一种以MAC为中心的LiM-HDL编译流程，可以将传统的布尔描述转换为可执行的MAC操作。为了确保功能正确性，采用了基于SAT等价的正式验证框架。实验结果表明，与现有的基于RRAM的逻辑综合方法相比，这种方法显著减少了计算周期，凸显了基于MAC的逻辑在新兴内存计算系统中的实用性。

**引言**
电阻式随机存取存储器（RRAM）是一种非易失性存储技术，其内部电阻状态可以编码二进制信息[1]。除了数据存储外，RRAM设备还能够在内存阵列中直接执行逻辑和算术操作，从而催生了内存计算范式。已经提出了多种基于RRAM的内存计算方法，这些方法通常依赖于通用逻辑原语，如材料蕴含（IMPLY）[2]、三多数投票（MAJ）[3][4]或忆阻辅助逻辑（MAGIC）[5]。虽然这些方法有效，但它们通常需要大量的写入周期或重复的内存刷新操作，并且未能充分利用RRAM交叉架构中的并行性。在交叉结构中，沿列流动的电流通过输入电压的求和自然实现了MAC操作，从而实现了对神经形态系统至关重要的矩阵向量乘法（MVM）[6][7][8][9]。更广泛地说，MAC操作提供了一种高吞吐量且本质上的并行计算机制，成为许多现代加速器架构的基础。然而，尽管具有潜力，基于MAC的方法在通用逻辑评估中的应用仍然有限。现有研究指出了根本性的效率低下问题。例如，基于二进制决策图（BDD）的MAC方法[10]仅使用了两个有效的交叉行，严重限制了并行性；同样，基于MAC的SAT求解器[11]也存在可扩展性挑战，限制了其在更大逻辑实例中的应用。虽然有研究提出了基于RRAM交叉架构的布尔逻辑评估方法[12]，但该方法缺乏系统的MAC计算抽象，并未完全解决大型复杂逻辑函数的可扩展性问题。

在本研究中，我们专注于RRAM交叉架构中MAC执行的计算方面，特别是实现更高抽象层次的计算。所需的外围电路（包括感测和转换组件）被假定为可用，并且能够与交叉架构的计算透明协作。

**当代硬件综合流程**
当前的硬件综合流程主要依赖于Verilog和VHDL等硬件描述语言（HDL）。这些语言使用自然映射到CMOS架构、寄存器、逻辑门、多路复用器和顺序逻辑的结构来描述数字系统。尽管标准HDL适用于常规数字设计，但它们无法捕捉支持LiM系统效率的架构特性。因此，使用传统HDL表达LiM计算会导致电路结构无法准确反映交叉架构的计算模型——在这种模型中，计算是通过跨行和列的精心编排的电压模式实现的。

为了解决这一抽象差距，先前的工作引入了LiM-HDL，这是一种与Verilog兼容的扩展，用于描述LiM架构[13][14][15]。在此基础上，我们提出了基于MAC的LiM-HDL，这是一种专门为基于MAC的内存计算设计的硬件描述语言。它包括对MAC基础微操作、初始化阶段以及MAC执行期间电流流动积累的抽象。由于这种方法完全基于HDL，因此保持了传统硬件开发的熟悉语法和设计方法。

**工作的动机**
MAC操作在现代计算中起着核心作用。MAC主导了神经网络处理、神经形态架构和向量-矩阵乘法器设计。在模拟RRAM交叉架构中，MAC是最自然且高效的计算方式。因此，将MAC扩展到数字逻辑领域是迈向未来计算系统的关键一步，在这些系统中，存储和计算将共同设计。通过基于MAC的微操作实现布尔计算，本研究有助于实现基于内存计算原理的下一代计算机架构的长期愿景。

**验证的需求**
随着基于交叉架构的设计规模的扩大，保证功能正确性变得越来越具有挑战性。对于具有大量输入和输出的较大系统，手动检查或基于仿真的验证方法是不够的。为了确保正确性，我们采用了等价性验证来比较基于MAC的交叉架构微操作实现的布尔函数与传统逻辑网络的布尔函数。虽然之前的研究已经考察了基于IMPLY、MAJ或MAGIC原语的正式验证[16][17]，或专注于验证OR-反相器图（OIG）级别的MAC描述[18]，但本工作首次引入了针对基于MAC的RRAM计算的微操作级别的验证。

随着嵌入式AI、边缘计算和实时信号处理等应用对高效能和高吞吐量架构的需求不断增加，基于RRAM的内存计算成为了一个有前景的选择。然而，进展受到了缺乏可扩展的综合流程和可靠验证框架的限制。通过使用MAC操作实现并行、高效且可形式验证的布尔计算，本研究为将基于RRAM的MAC加速器集成到更大的计算系统中奠定了完整的基础，并为下一代计算平台实现可重构、低延迟的内存架构做出了贡献。

**技术细节**
RRAM固有的模拟计算能力使其相对于其他新兴存储技术具有显著优势。这一独特特性对于高效的MAC操作尤为重要，而MAC操作是矩阵向量乘法（MVM）的计算基础，这是神经网络实现的基本要求。如图1所示，交叉架构中的RRAM设备会使用相当于矩阵元素逆值的电阻值进行精确初始化（rj,k = gj,k?1）。

**提出的LiM HDL映射和验证方法**
本节分为三个部分：首先讨论基于MAC的映射方法，然后探讨基于MAC的LiM HDL，最后描述验证过程。整个过程的概述见图2。

**实验评估**
本节评估了所提出的基于MAC的映射和验证框架，重点关注计算效率和功能正确性。我们评估了该方法在各种基准测试中的效率和可扩展性，并将结果与代表性的内存计算范式（如MAJ、MAGIC、LiM-HDL和AIG实现）进行了比较。此外，我们还验证了验证流程的正确性和性能，证明了所提方法的有效性。

**交叉架构约束和可扩展性**
虽然基于MAC的LiM-HDL框架在执行延迟和计算并行性方面取得了显著改进，但其实际实现受到RRAM交叉架构物理限制的制约。特别是，大型单体交叉架构存在非理想效应，如漏电流、互连寄生效应和器件变异性，这些因素会随着阵列尺寸的增大而降低信号完整性和可靠性[8][31]。

**总结与结论**
本文提出了一种适用于RRAM交叉架构的基于MAC的内存计算综合与验证框架。通过将布尔逻辑综合与交叉架构的固有乘法-累加行为对齐，该框架弥合了传统HDL设计方法与新兴内存计算范式之间的差距。通过Yosys中的Oigmap和Macmap pass实现的基于MAC的LiM-HDL流程，实现了这一目标。

**作者利益声明**
作者声明没有已知的会影响到本文工作的财务利益或个人关系。

**致谢**
本研究部分得到了德国研究基金会（DFG）项目PLiM（DR 287/35-1, DR 287/35-2 和 SH 1917/1-2）以及印度科技部（DST）、德国联邦教育和研究部（BMBF）和德国学术交流服务（DAAD）共同资助的印德项目的支持（DST编号86669，DAAD编号57682048）。

法特梅赫·希林扎德（Fatemeh Shirinzadeh）毕业于伊朗塔布里兹大学，获得电信工程硕士学位。她目前是德国人工智能研究中心（DFKI）的研究员，并在不来梅大学攻读计算机架构博士学位，导师为罗尔夫·德雷克斯勒教授。她的研究方向包括内存计算、内存测试和验证。