在线研讨会预告：Formal DPV在嵌入式AI处理器的案例验证

2023-03-19 22:03

我们生活在大数据的世界中：B站日均播放量17亿次，微信每天发送约500亿条信息。如此庞大的数据量，需要采用浮点算术运算的芯片才能够以最快的速度和最高的精度进行处理、存储、分析和共享。而验证这些芯片上的数据处理逻辑（数据路径）的正确性至关重要。历史证明，未能及时发现错误将会导致高昂的代价。

基于仿真的传统验证方法效率低、耗时长，而且对于无遗漏地验证这些复杂的数学函数根本不切实际。以一个两个32位操作数的简单数学运算为例子，其中就会包含264个操作数。假设处理速度为每秒30亿次模拟速度，则需要195个计算年。这导致计算资源根本无法得到充分和高效利用。

鉴于此，新思科技很早就开始研究验证复杂数据路径逻辑的方法，并推出了业界首个用于对数据路径元素进行无遗漏验证的商用形式验证工具 VC Formal® Datapath Validation (DPV) 。

VC Formal DPV 可以针对独立开发的模型提供等效性检查，无遗漏地验证 RTL 实现是否与可信的 C/C++ 参考模型等效，并且可用于无遗漏地验证 C 到 C、C 到 RTL，以及 RTL 到 RTL 等连续设计改进，而无需任何验证平台、断言或覆盖率要求。

3月21日下午14点，新思科技联合智东西公开课策划推出的「新思科技 VC Formal DPV 在线研讨会」将正式开启，新思科技验证团队高级应用工程师李霈霈、解决方案事业部门高级验证工程师蒋帅宇两位主讲人将进行直播讲解。

在此次研讨会上，新思科技解决方案事业部门高级验证工程师蒋帅宇将以《Formal DPV 在嵌入式 AI 处理器的案例验证》为主题，介绍新思科技 ARC® NPX 嵌入式 AI 处理器系列 IP 及使用 VC Formal DPV 验证该系列 IP 数据通路功能。从而了解新思科技 ARC NPX6 处理器所支持的最新和最复杂的 CNN 和 RNN 神经网络。

NPX6 神经网络处理器的核心是卷积和 Tensor 加速器，它们被优化设计以执行高效计算。这些功能单元的正确性对于面部、音频、图像处理和识别的正确性至关重要，这可能也对汽车应用产生安全影响。这项处理器方案已广泛应用于汽车，数据中心，高端游戏，下一代增强现实和监控的 AI SoCs中。

蒋帅宇拥有7年数字前端验证经验，目前负责新思科技 ARC NPX6 产品验证工作。