从C/C++到RTL,提速100倍的形式化验证加快AI算法到芯片的迭代

VC Formal数据通路验证应用基于形式化方法学，在C/C++算法和RTL设计实现之间的一致性检查方面比传统技术提高了100多倍。

采用芯片业界公认的的HECTOR先进技术，并且集成了以Verdi界面为基础的VC Formal的多样化调试功能。

新思科技近日推出了数据通路验证(DPV)应用，这是其VC Formal®解决方案的一部分。数据通路验证应用采用芯片业界公认的HECTOR™先进技术，在设计和验证周期内为广大的数据通路密集型设计用户提供完备的形式化验证收敛。该应用基于形式化方法学，其在C/C++算法和RTL设计实现之间的一致性检查上比传统的复杂芯片系统(SoC)设计技术快100多倍，并且支持遍历式验证确保设计的正确性。

“我们的使命是为移动芯片应用开发高质量的CPU、GPU和系统IP，这就要求在非常紧的时间内实现具有高度竞争力的功能、卓越的整体性能和极低的功耗。C/C++算法与具体RTL设计实现的一致性形式化方法学为我们以数据通路为主的设计提供完备的验证，以便在几分钟内有效地发现很多极端应用场景下触发的设计错误，而使用其他传统仿真技术是不可能做到的。VC Formal的HECTOR技术提供同类最佳的表现和结果质量，能够成功减少传统仿真工作量，并帮助在设计中捕获30多个RTL错误。”——Xiushan Feng

”人工智能(AI)、图形和处理器设计涉及复杂的算法功能模块，其数据通路量很大，需要用C/C++等高级语言对它们的行为进行建模。这些设计所实现的RTL因此需要与其对应的C/C++模型进行功能等价性验证。VC Formal与Verdi®自动调试系统的内在集成使设计和验证团队能够轻松地使用形式化验证技术和自动对形式化结果根源分析功能。此外，VCS在VC Formal中的内在集成便于将形式化分析融入到现有的验证环境中。

数据通路验证应用加入了不断增长的VC Formal应用组合中，其还包括属性验证(FPV)、时序电路等价验证(SEQ)、寄存器验证(FRV)、形式化覆盖分析器(FCA)、连接性检查(CC)、X-Propogation检查(FXP)、形式化Testbench分析器(FTA)、属性自动提取(AEP)和回归模式加速器(RMA)。

“越来越多的数据通路密集型设计需要专门的数据通路验证技术来实现更快的验证收敛。我们长期以来一直与业界领头羊合作，为先进的芯片提供全面的验证解决方案。我们在数据通路验证技术上的投资能够更快地帮助用户完成算法验证，并加快其芯片产品上市时间。”——Ajay Singh