新思科技VC Formal DPV可对任何数据路径块进行签核

　　我们生活在大数据的世界中：B站日均播放量17亿次，微信每天发送约500亿条信息。预计到2025年，全球每天生成的数据量有望达到463EB。

　　如此庞大的数据量，需要采用浮点算术运算的芯片才能够以最快的速度和最高的精度进行处理、存储、分析和共享。而验证这些芯片上的数据处理逻辑（数据路径）的正确性至关重要。历史证明，未能及时发现错误将会导致高昂的代价。

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

　　形式验证使用数学方法来证明或反驳预期算法的正确性，可提供一种有效、高效且可追溯的解决方案。在对函数正确性至关重要的复杂控制和数据路径逻辑进行验证时，它可对仿真方法起到补充作用。认识到设计架构师趋向于将规范编写为C或C++参考模型，新思科技的研究团队开始致力于开发一种验证技术来确定硬件设计人员创建的RTL是否等效于C/C++模型。复杂数据路径专用验证解决方案HECTOR（High-level Equivalence C++ to RTL）由此诞生。

　　过去20年间，新思科技不断升级形式求解器，性能越来越完善，促使许多客户开始使用HECTOR来验证CPU、GPU、网络和安全性应用中的ALU、FPU和DSP块。2017中，HECTOR技术被整合到新思科技 VC Formal® Datapath Validation （DPV） App中，该应用现已能够支持所有现代C++语言和基于业界领先的新思科技 Verdi® SoC Debug Platform的完整调试环境。VC Formal DPV成为业界首个用于对数据路径元素进行无遗漏验证的商用形式验证工具。

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

　　快速高效的形式算法，包括加入多个求解器用于解算复杂的数学逻辑

　　快速收敛技术，包括自动设计分区和多处理器支持

　　高级调试支持，包括一个集成的调试器，支持单步调试C/C++代码

　　灵活的语言支持：Verilog、VHDL、SystemVerilog、C、C++

　　VC Formal DPV可提供100%的信任度，其RTL设计实现符合C/C++参考算法，因此与基于仿真的技术相比，可以显著加快数据路径组件的签核。

　　随着电子设备变得越来越智能，人工智能（AI）和机器学习（ML）芯片被广泛应用于许多领域。由于AI/ML芯片使用浮点运算来处理大量数据，因此VC Formal DPV非常适合此类芯片设计，获得了全球AI/ML初创企业的大量部署。

　　为了帮助企业采用数据路径验证方法，新思科技提供了经过形式验证的全面的C++数学库来验证RTL，并且还为交钥匙项目的培训和执行提供咨询服务。

　　数据路径验证的前景十分光明。新思科技凭借20多年的HECTOR技术投入和不断革新，其VC Formal DPV可对任何数据路径块进行签核。

　　审核编辑：彭菁