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

Synopsys Editorial Staff

Jun 09, 2021 / 1 min read

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

机器学习1

智能化在我们的生活中日益普及,从便携式音响到工厂设备、医疗器械到汽车,随处可见其身影。人工智能(AI)和机器学习(ML)应用领域的芯片市场也随之发展壮大,无论是初创公司还是大型企业,纷纷加入这场角逐。

AI/ML以及CPU/GPU设计均涉及大量带有数据路径逻辑的算术计算,包括所有传统的算术和逻辑函数、浮点运算和数字信号处理(DSP)算法。数据路径验证是确保设计没有缺陷并能达到严格流片标准的关键所在。若要对复杂的数据路径设计进行无遗漏验证,HECTOR技术是其中最高效的一种技术

问:什么是数据路径验证?它有多重要?

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显著加快了数据路径组件的签核。

vc 正式 dpv 1

对于许多开发者来说,创建参考模型是等效性检查环节的难点之一。许多公司已经采用以可信的C++参考模型作为起点的设计流程。即便开发者没有这样的设计流程,新思科技也能提供一个经过形式验证的综合性C++数学库,供开发者用于验证 RTL。

欲了解更多关于HECTOR技术,不要错过我们为你准备的《芯课程》。导师将介绍如何使用新思科技VC Formal DPV来加速收敛这类运算器的验证。并且将演示如何对C/C++ 模型和RTL设计进行形式等效性检查, 达到完整高效的验证。>> 报名链接

Continue Reading