高级验证：开启人工智能芯片新时代的大门

“嘿 Siri，今天的天气预报是什么？”

随着我们的日常生活继续依赖 Siri 和其他人工智能 (AI) 助手提供方便的服务，例如播放歌曲和跟踪会议日程，保护个人数据变得越来越困难已不是什么秘密。随着 AI 势头的增强和数据丢失的威胁迫在眉睫，芯片设计人员比以往任何时候都更重要的是推进 AI 和安全技术，以满足对更多智能的迫切需求。

但在当今万物智能的时代，结合深度学习 (DL) 和机器学习 (ML) 等人工智能技术的计算密集型应用需要自己的专用芯片，其设计全面，为智能功能提供动力。从自动驾驶汽车到高性能计算 (HPC)，驱动这些密集型工作负载的底层技术取决于先进的架构，这些架构在电力部门发挥作用的同时也为提高决策能力而量身定制。

随着越来越多的智能设备连接到云端，AI 呈指数级发展并创造各种市场机会的潜力越来越大。然而，芯片制造商必须牢记，人工智能计算的关键部分需要在硬件中完成，以模拟现实世界的条件。因此，定制“人工智能芯片”不仅是首选，而且对于以经济高效的方式大规模集成人工智能也是必不可少的。

但考虑到当前用于 AI/ML/DL 应用程序的芯片包含复杂的数据路径以准确执行必要的算术分析，行业将必须愿意并准备实施先进的验证方法来发展和推动 AI 的下一步发展。

几乎每个人都在设计芯片

在芯片设计领域，随着摩尔定律的饱和，从通用处理器获得预期的性能增益变得越来越困难，这在芯片设计领域已不是什么秘密。为了缓解这种放缓的影响，传统半导体厂商以外的公司纷纷将自己的帽子放在芯片设计领域。

仅举几例，谷歌、亚马逊和 Facebook 等大公司现在都在大力投资开发自己的内部定制 ASIC（专用集成电路）芯片，以支持其独特的 AI 软件并满足特定应用要求。随后的市场扩张为新的设计工具和解决方案提供了大量机会，以支持当今要求苛刻的芯片设计环境。

AI芯片设计：控制路径不同

新 AI 片上系统 (SoC) 投资的一个关键驱动因素是以分布式方式同时进行多任务计算的能力（而不是传统 CPU 提供的有限并行性）。执行这些任务所需的设计需要由控制路径组成的数据密集型块，状态机在其中处理基于特定输入的输出，以及由算术逻辑组成的计算块以处理数据。通过利用这些特性，芯片设计人员可以显着加速 AI 算法所需的相同、可预测和独立的计算。

尽管算术计算块通常不是一个挑战，但随着算术块和位的数量同时增加，复杂性会严重增加，从而进一步增加了验证团队的负担。

在过去十年中，以数据为中心的计算已经超越了 PC 和服务器的限制。即使在 4 位乘法器的简单情况下，也需要为所有可能的输入组合编写测试向量以验证其完整功能，即 2 ⁴ =16. 这就是挑战：在验证当今 AI 芯片的真实场景时，团队需要验证具有 64 位输入的加法器。换句话说，2 ⁶⁴ 状态需要得到验证——使用经典方法需要数年才能取得成就。这只是众多可能性中的一个孤立示例，但随着 AI 芯片的采用迅速扩大和生成的数据量持续爆炸式增长，与硬件验证相关的耗时挑战使得对现代、安全和灵活的验证解决方案的需求变得至关重要.

终极测试：验证挑战

团队在设计 AI 芯片时，会使用 C/C++ 这种快速且广泛使用的设计算法。一旦编写了功能代码，就需要使用 RTL（寄存器传输语言）将信息转换为更面向硬件的表示。这个过程要求团队要么为所有可能的组合开发测试向量，要么比较 RTL 是否与原始 C/C++ 架构模型匹配，这通常被证明是一项非常艰巨的任务。

这就是形式验证发挥作用的地方。使用这种技术，可以进行数学分析以一次性考虑整个硬件设计。虽然通常需要为每个输入组合编写测试向量，但形式验证提供了一个渠道，通过利用模型检查器来验证一组指定预期行为的断言。

即使在几年前，仅仅因为需要高级断言，就认为形式验证可以成为一种广泛使用的方法也是不可想象的。但快进到今天，普通的 RTL 设计人员或验证工程师可以快速有效地学习行业技巧。

然而，基于当今人工智能芯片不断增长的规模和复杂性，仅通过模型检查是不可能完全证明的。使用传统方法而不是现代方法验证这些数学函数效率低下、耗时，而且从长远来看最终是不切实际的。

AI 和 ML 应用程序需要额外的帮助

使用其他形式的形式验证（例如，等效性检查）为工程师提供了一个强大的系统来验证最复杂的 AI 数据路径。在等效性检查过程中，对设计的两种表示进行比较，然后证明设计是等效的，或者确定它们之间的具体差异。这些足够强大的形式引擎在验证过程中提供了很大的帮助，因为这两种表示可以处于完全不同的抽象级别，甚至可以用不同的语言编写。

让我们将芯片设计的详细 RTL 实现与高级 C/C++ 架构模型进行比较。比较确认同一组输入为两种表示产生相同的输出。鉴于大多数已经拥有 C/C++ 模型可用于仿真结果检查或作为支持早期软件开发和测试的虚拟平台的一部分，这种高效的方法自然适合许多 AI 项目。

尽管 AI 应用程序快速增长，但形式等效性检查是唯一可以针对经过验证的参考模型对设计数据路径进行详尽验证的技术。为了帮助 AI 迄今为止不受约束的发展，验证工具需要具备以下特征：易用性、扩展能力和高级调试能力。

即将到来：同态加密

随着行业继续产生数万亿字节的数据，需要高性能芯片来维持这一计算壮举，因此不可避免地会出现比特数的增加。世界各地的大学和研究机构都在研究处理大量输入数据的可能性，并制定应急计划来设计能够支持这种涌入的芯片。

但是，随着数据的泛滥，随之而来的是对硬件安全性的需求。同态加密将成为 AI/ML 难题的组成部分。这种类型的加密使芯片设计人员能够加密数据并执行 AI 系统所需的相同算术计算，而无需对其进行解密，从而降低数据泄露的风险。为了通过这种加密系统提高 AI 芯片设计的结果质量和生产力，将需要下一代工具。

边缘人工智能将推动实时海量数据计算爆炸式增长

自动驾驶汽车撞上无人注意的障碍物不在任何人的愿望清单上。如果设计没有得到完全验证，这只是 AI 芯片可能造成的灾难的一个例子。随着市场对计算应用程序中更多 AI 功能的需求不断增长，新的边缘 AI 设备将推动实时大量数据计算的爆炸式增长，并改变芯片制造商处理半导体设计的方式，从而提高生产力、更快的周转时间和更好的验证解决方案。

人工智能优先世界的曙光正在迅速临近，而且比以往任何时候都更加触手可及。但是我们能否在创新仓鼠轮上运行足够长的时间来实现它？只有时间会证明一切。