中文 英语
18lickc新利
的意见

汽车应用中AI处理器数据路径的正式验证

数据路径中的错误可能会导致芯片行为不当,就像状态机中的错误一样。

受欢迎程度

没有多少电子应用比汽车和其他道路车辆更需要正确性、安全性和安全性。车主们都希望自己的汽车在任何时候都能正常可靠地运行。如果车辆行为不端,司机、乘客和附近的人都有生命危险。

随着汽车电子产品的每一次创新,这种情况都变得更加严重。随着现代先进的驾驶辅助系统(ADAS),汽车在驾驶时间的部分控制。司机可能有时间来纠正不安全的情况,但随着自动驾驶水平的提高,这种可能性越来越小。

当真正的自动驾驶汽车到来的时候,很可能根本就没有人工控制,所以人类干预将是不可能的。一切都取决于电子设计的正确性,以及系统的安全性。

α粒子翻转内存位或硅老化效应不能影响操作。功能安全标准,如ISO 26262,要求检测故障并纠正或消除故障。此外,系统必须安全,不受恶意代理的攻击,这些恶意代理可能会像芯片故障一样危及生命。

这些严格的要求对汽车电子产品的验证过程提出了巨大的要求。工程师必须确保他们的设计是正确的,安全的,在他们部署在现场之前。不幸的是,包括ADAS和自动驾驶在内的同样的趋势使得验证变得更加重要,也使得设计更加难以验证。

现在的汽车不仅仅包含伺服系统和简单的微控制器。当今电子控制单元(ecu)中使用的芯片是世界上最大、最复杂的芯片之一。它们包括具有并行数据路径和深层管道的高度复杂的处理器。人工智能(AI),尤其是机器学习(ML),在先进的交通系统中发挥着巨大的作用,需要强大的处理器。

当需要确定性时,芯片开发团队会考虑正式的验证。与基于模拟的测试不同,形式化算法证明设计在所有可能的情况下都是正确的。这保证了验证团队不会忘记编写一个特定的测试,从而错过了一个设计错误,因为一些功能从未被检查过。

将形式化验证应用于现代汽车电子产品中使用的复杂流水线AI处理芯片可能不是一个明显的解决方案。从历史上看,形式化方法被认为更适合于控制逻辑而不是数据路径。

然而,数据路径中的错误可能会导致芯片行为不当,就像状态机中的错误一样。有一些众所周知的设计缺陷的例子,其中一个特定算术操作的一小部分操作数产生了错误的答案。在汽车芯片中,一个错误的答案可能导致灾难。

当工程师谈论形式化验证时,他们通常想到的是证明设计与定义预期行为的一组断言或属性相匹配。这种方法适用于控制逻辑,但对数据路径来说更具挑战性。对于算术运算,在输入和输出之间有大量的路径,因此在数学上考虑每种可能的场景是计算密集型的。

幸运的是,事实证明有一种更简单的方法来验证ecu中的AI处理器数据路径。形式化算法可以用来证明寄存器传输级(RTL)设计与用C/ c++在更高功能级别编写的规范相匹配。这样的参考模型实际上已经存在于每个芯片项目中,因为它们被用于架构分析和软件开发。

最近的一次网络研讨会给出了一个用形式化解验证有限脉冲响应(FIR)滤波器的例子,该滤波器累积了一系列的乘法结果。这种滤波器可能会出现在汽车电子系统中,作为雷达系统的一部分,提供对周围环境的洞察,并测量与附近物体的距离。FIR滤波器是其他类型数据路径的代表,因为它的最终结果取决于之前的结果。

FIR滤波器的另一个有趣的方面是,它们可以与所有乘数并行实现,一个乘数可以在多个循环中重用,或者是两者的混合。形式验证同样适用于所有这些实现。网络研讨会中使用的FIR4设计包含四个乘数。由于它们是相同的,所选择的方法首先验证了单个乘法器,然后将结果应用于整个设计。

在C/ c++中,乘数的功能可以简单地表示为“a * b”,其中变量表示乘数和乘数。利用Synopsys VC形式化解决方案及其数据路径验证(Datapath Validation, DPV) App证明了乘法器的RTL实现与C/ c++表达式匹配。这只需要最小的设置,主要是在两个表示之间映射输入和输出。

一旦乘数被证明是正确的,假设保证方法被用于整个FIR设计。通过假设每个乘法器的输出是其输入的乘积,可以抽象出RTL实现的细节。对剩余RTL的形式化分析非常高效,并证明了整个FIR设计与预期功能的C/ c++参考模型相匹配。

这种方法非常灵活,既支持手写的C/ c++模型,也支持由MathWorks MATLAB环境生成的模型。支持所有常见的数据路径操作,包括加、减、乘、除和平方根。假设-保证方法将解决方案扩展到任何复杂的设计,包括cpu、gpu、dsp和AI/ML应用程序中常见的卷积神经网络(cnn)。

Synopsys VC正式DPV为数据路径设计提供了详尽的验证,包括ecu和其他关键应用中的数据路径设计。开发人员可以在不需要任何测试台架的情况下实现数据路径签名。有关这个业界领先的解决方案的更多信息,以及FIR滤波器验证示例的完整细节,请观看网络研讨会在这里



留下回复


(注:此名称将公开显示)

Baidu