随着人工智能和物联网技术的蓬勃发展,用于加速神经网络计算的神经网络处理单元（Neural network Processing Unit,NPU）逐渐成为系统级芯片研发热门领域。高性能NPU的设计复杂性也给验证工作带来巨大挑战,尤其是运算处理和内存访问这类复杂逻辑单元。传统模拟仿真验证方法耗时低效的同时也存在难以保证功能验证完备性的问题,进一步导致极端缺陷逃逸。所以应用高效的形式验证方法来对运算处理和内存访问核心单元进行更加完备的验证就显得非常有必要。本文针对某款高性能低功耗NPU内核的运算处理和内存访问单元验证工作,主要做了以下两方面的改进。1)提出了一种适用于复杂的数据路径模块的高效等价性验证方法。针对内核运算处理单元,首先,基于Python环境对其所支持的神经网络运算类型的C++参考模型,完成随机验证。其次,对卷积数据通路conv2d单元,针对其中4个纯组合逻辑子模块,编写TCL脚本实现对应功能逻辑。再次利用数据路径验证（DataPath Validation,DPV）方法来充分验证不同配置下conv2d单元设计的功能正确性。最后针对激活数据通路中32位Booth乘法逻辑存在证明无法收敛的问题,采用等效-级联证明方法得到解决。2)提出了一种利用分解-抽象模型来完成内存访问单元DMA模块的形式验证Signoff方法。针对内存访问单元,首先利用AXIAIP搭建了 AXI2AXI bridges的形式验证环境,完成对应模块断言检查属性的设计实现,并利用形式属性验证（Formal Property Verification,FPV）方法验证所有的检查属性都达到了所需证明深度,完成了 AXI2AXI bridges三个模块的功能验证。其次通过分析DMA模块属性检查过程中遇到的不确定性证明结果,采用数据传输抽象和地址抽象的方法简化逻辑,使形式探索的深度达到了对应的有界性证明阈值。最后完成DMA的有界性形式属性验证Signoff,确保内存访问单元的功能实现得到了详尽验证。本文在进行形式验证的过程中,针对激活数据通路中复杂Booth乘法的等价性验证,传统形式验证方案运行长时间后无法证明该硬等价问题,而采用等效-级联证明方法后仅用3625秒就成功得到解决。其次针对DMA形式验证中不确定或有界性证明结果,未采用分解-抽象模型复杂化管理方法时,形式引擎探索内部状态机计数器更新2次需要遍历40～50个时钟周期,在采用分解-抽象模型方法后缩减到10～15个周期,并由此发现了在子系统验证中遗漏的3个极端角落Bug。这些方法可以给目前行业内面临的挑战性验证任务如何应用形式验证去解决提供一定参考。