用高效技术拯救复杂数据路径验证，浅谈HECTOR技术

作者：新思科技验证事业部研发总监Pratik Mahajan，新思科技科学家 Alfred Koelbl, 新思科技高级产品营销主管 Kiran Vittal

问：什么是数据路径验证？它有多重要？

CPU、GPU和AI硬件等使用浮点运算的芯片可以处理数百万次高度精确的计算。它们必须具备复杂的数据路径才能执行这种数学分析。然而，数据路径中会有无法检测到的极端缺陷，从而引发系统故障。以火箭轨道的计算为例，浮点单元(FPU)中的一个细微缺陷都可能导致火箭坠毁。数据路径验证的不断推进，就是为了识别此类缺陷。

问：什么是HECTOR技术？为何对数据路径验证有用？

HECTOR，全称High-level Equivalence C++ to RTL，表示高级C++到RTL等效性检查，隶属新思科技VC Formal产品系列。市面上现有的大多数形式验证工具都只关注控制逻辑的验证。而HECTOR技术是市面上唯一可用于无遗漏验证数据路径元素的形式验证工具，该技术包含用于数据路径验证的自定义引擎，可验证算术逻辑单元(ALU)、FPU和DSP模块。

问：HECTOR技术如何帮助简化数据路径验证的艰巨任务？

HECTOR技术针对独立开发的模型提供等效性检查，无遗漏地验证了RTL实现是否与可信的C/C++参考模型等效。还可用于无遗漏地验证C到C、C到RTL，以及RTL 到RTL等连续设计改进，无需任何验证平台、断言或覆盖率要求，且能灵敏地检测极端缺陷。该技术嵌入了：

• 快速高效的形式算法，包括加入多个求解器用于解算复杂的数学逻辑
• 快速收敛技术，包括自动设计分区和多处理器支持
• 高级调试支持，包括一个集成的调试器，支持单步调试C/C++代码
• 以及灵活的语言支持：Verilog、VHDL、SystemVerilog、C、C++14/17

HECTOR的RTL设计实现符合C/C++参考算法，与基于仿真的技术相比，HECTOR显著加快了数据路径组件的签核。