18lickc新利
的意见

更快的形式验证关闭datapath公司的人工智能设计

使用RTL设计之间的等价性检查和C / c++模型设计的功能验证复杂的datapath公司。

受欢迎程度

近年来,许多长期存在的对形式验证的假设变得过时了不断完善的技术。应用,如连通性检查表明,正式可以在大型芯片系统(SoC)的设计工作,而不仅仅是小块。标准SystemVerilog断言(上海广电)消除了需要为每个新正式学习一个深奥的数学语言工具。或许最令人惊讶的早期正式用户只关注控制逻辑的方法来验证复杂datapath公司的发展。浮点运算,数字信号处理(DSP)甚至卷积神经网络(cnn)今天正式被验证。

这个创新的时机不可能更好。现在许多的应用程序驱动半导体行业是数学,尤其是将人工智能(AI)技术,如深度学习。每个人的最喜欢的例子似乎是自动驾驶汽车。他们强烈要求图像识别、机器学习和传感器集成意味着芯片自动车辆是复杂的,有挑战性的验证计算datapath公司。只有正式的方法可以进行详尽的验证和提供必要的信心程度。

Synopsys对此datapath公司已经开发了一个新的方法验证,依赖之间的等价性检查寄存器传输级(RTL)设计和C / c++模型设计的功能。许多芯片项目这样一个模型的虚拟平台,支持早期的软件开发和测试。也有众多的开源库,实现常见的算术函数,如伯克利SoftFloat IEEE 754浮点标准包。C / c++模型通常是在更高的抽象层次的RTL实现匹配的端到端功能但没有时间或其他硬件的细节。

传统的等价性检查不能处理比较RTL和C / c++等模型。组合/逻辑等价跳棋依赖模型匹配状态元素(注册/拖鞋/记忆)和通常用于比较的RTL输入和网表输出逻辑综合工具。连续的等价跳棋允许状态差异模型和检查在每个时钟周期等于输入等于产出。因为C / c++模型不是cycle-accurate,可能完全不计时的,事务等价性检查是必需的。这种技术检查的结果等于输入只有最后的一个事务,比如多循环算术运算。


图1:不同形式的等价性检查

Synopsys对此VC正式Datapath公司验证事务(第一项)应用等价性检查和验证复杂的Datapath公司的权力。是用于DSP引擎,浮点单元(型),图形处理单元(gpu), cnn和其他元素在人工智能应用程序使用。它支持所有常见的算术运算,包括如部门和平方根迭代计算。它使用Synopsys对此赫克托耳一流技术、等价性检查的一个行之有效的解决方案的挑战。第一项应用程序包含自定义优化和引擎调优的主要任务比较交易的结果。

使用作为一个例子,考虑一个乘数。其操作可以模仿非常在C代码,例如用一个函数调用,如“结果=乘(a, b)”的抽象模型。然而,实现可能需要数百行RTL代码以捕获特定的算法。RTL计算可能需要多个周期才能完成,而C / c++的结果是不计时的,立即可用。事务等价性检查忽略这些细节和检查结果同意只有当两者都准备好了。如果找到任何分歧的情况下,第一项应用程序提供详细信息和直观的图形用户界面(GUI)在Synopsys对此威尔第SoC调试平台,追踪差异的原因。一旦一个完整的证明报告,设计和验证团队确定的两个模型在任何情况下产生相同的事务的结果。


图2:Datapath公司验证(第一项)应用程序流

不同于其他形式的等价性检查,第一项应用程序不需要任何通信状态元素之间的两种模型相比较。然而,如果可以匹配的状态,这可以提高性能通过降低比较困难。容量和性能受到交易的长度的影响。没有固定的上限,但所有事务的长度必须是有界的,这样可以比较的结果。第一项应用程序是专门设计用于datapath公司,虽然它可以处理包含datapath公司和控制功能的设计。设计的大小也会影响性能;技术是最好的作为块级验证的解决方案。

第一项应用程序可以用来比较两个C / c++模型或两个RTL模型,除了比较每个之一。这证明了独立开发的一致性模型,例如确保IEEE 754的内容在一个定制的C / c++模型匹配SoftFloat等参考实现。连续在RTL阶段,可以验证设计细化详尽即使修改后的设计变更部分的长度的事务。


图3第一项应用:多个用途

第一项应用程序已成功地应用在许多不同类型的datapath公司。在Synopsys对此,DesignWare团队使用应用程序来验证复杂的知识产权产品,包括型、嵌入式视觉处理器和CNN引擎。三星不仅GPU和CPU的团队和先进的计算机实验室报道赫克托耳,VC正式的技术减少了仿真工作,并帮助捕获超过30 RTL datapath-centric设计缺陷。此外,一家领先的专业图形公司没有发现post-silicon bug部署后的第一项应用验证流程。与此形成强烈对比的一个用于设计十多个datapath公司在硅bug被发现。这些例子演示事务等价性检查提供的巨大的价值。

datapath公司需要详尽的验证用于自主车辆、医疗电子产品和其他关键的应用程序。Synopsys对此VC正式第一项应用结合强大的小说与一个用户友好的GUI提供正式解决和证明的解决方案。更多信息,包括演示可用的网络研讨会



留下一个回复


(注意:这个名字会显示公开)

Baidu