FPGA形式化验证工具OneSpin360™新版发布

时间:2024-03-06 21:32:40

在这里插入图片描述

Onespin是领先的EDA解决方案提供商,其360系列产品为FPGA形式化验证工具。它以强大、高性能的形式化验证引擎为基础,能够覆盖自动设计分析到高级属性检查以及逻辑等效性验证,帮助构建功能正确,安全,可靠、可信赖的系统。

OneSpin 360™2020.2.0版本现已准备就绪,该版本包括功能和性能方面的改进。新增与增强的功能有:

● 新的编译器和优化程序:这些改进了工具所有部分的性能,包括更快的工具启动,设计编译和GUI交互。

● 新的FSM指示器:如下所示,此新指示器提供了更高级的界面来调试和理解FSM。它允许按状态过滤状态,并且能够交互式地自定义状态布局。

 

在这里插入图片描述

 

● 新的形式化引擎:新引擎在履行设计限制的同时,其行为就像是随机模拟器。它可以很好地按顺序解决深度属性,并且在某些属性上已证明比现有引擎快300倍以上。与以前的默认引擎设置相比,它还可以在属性检查上并行运行,可检查的属性数量增加了10倍以上。

● 对SystemC附加构造的支持:扩展的构造支持包括自动插入等待状态以打破循环。

新版发行的具体内容如下:

OneSpin 360™常用功能的新功能

▷ 支持VHDL物理类型“时间”。
▷ SystemVerilog类支持已得到改进。
▷ SystemC现在支持C++ 14,包括std::array和std::tuple。所有从C++到14的语法改进,例如SCIN < ScIt< 10 >的双角括号也可用。
▷ 大大提高了编译命令的运行时间,运行效率的改善高达几个数量级。

图形用户界面中的新功能

▷ 从2020.2版本开始,FSM表中的状态可使用拖放手势。手势生成的是所有onespin shell命令可接受状态的字符串类型名称。

▷ 通过上下文菜单功能增强了属性调试器。自该版本发布以来,信号可以被跟踪,添加到波形中或在其他查看器中显示。

▷ 从此版本开始,打开代码查看器后,调试器的响应能力明显包括了新的触发器类别。信任问题管理器中的问题现在可以从视图中排除与/或导出到CSV。状态机的死锁情况现在会在信任问题管理器中报告。

OneSpin 360™设计验证的新功能

▷ 新的随机模拟引擎:disprover6。这个新引擎已添加到用于坚持和整数检查的默认配置中。也可以添加到prove配置中。例如:“check -prover_exec_order {{approver2 disprover6}} my_property”。

▷ 现在可以直接创建SVA模块,而无需使用create_sva_module -no_read_sva读取。

▷ 改进了截断和固定溢出检查的显示名称。例如:“ @ truncation @@ / local/TEST/dut.sv@16:1”到“ truncation_check_1”。

▷ 覆盖关闭加速器(CCA)应用程序已增强了与受支持模拟器的集成。

▷ FPU应用程序现在支持生成溢出异常以转换为整数。

▷ 处理器架构和验证应用已发布。

▷ 信任评估平台(TAP)应用程序具有以下增强功能:默认情况下,不会报告冗余分配带来的可靠性问题。运行analyze_trust -category reliability_assign指令以观察问题。信任问题管理器现在已自动启动。如果查看器关闭,则可以使用launch_trust启动报告视图,新命令export_trust可以用于生成CSV文件以进行脱机处理/分析,analytics_trust包括新的触发器类别。可以将信任问题管理器中的问题排除在视图之外与/或导出到CSV。

360 EC-FPGA的新功能

▷ OneSpin 360™现在包括针对以Max 10目标器件为目标的Quartus Prime Standard™实施流程的全面综合验证支持。

▷ 通过Virtex、Kintex和Zynq系列芯片对Xilinx Vivado的综合验证支持现在包括对状态的自动映射,其中Xilinx Vivado™生成的netlist名称依赖于分配的范围。此外,OneSpin 360™ 现在已经改进了分布式ram的状态映射,比如RAM32M和RAM64M内存块。

▷ OneSpin 360™的新指令analytics_clock_mapping,可通过查找映射到非时钟的时钟来帮助用户确定错误的设计设置。

▷ OneSpin 360™具有一项新功能,实现相同功能的映射RAM会被自动黑盒,这是一个抽象的概念,它可以显著提高可伸缩性。

▷ OneSpin 360™现在提供工具认证套件与实施流一起使用,该实施流是基于Synopsys Synplify™(G-2012.09A-SP4版本)进行合成和MicroChip Libero IDE™(9.2版本)反熔丝芯片(SX-A™、eX™、MX™和Axcelerator™系列)。

OneSpin 360™常用功能的已修复问题

▷ 修正了在调整FSM表格的大小期间可能偶尔发生的显示问题。

▷ 修复了一些窗口可能被缩小为零的问题。现在,所有窗口和选项卡都具有最小尺寸。

▷ 新的FSM可视化GUI。更好的FSM气泡默认设置以及交互式重新排序。可用的过滤器可以更好地可视化状态。

局限性

▷ Windows版本不支持OneSpin 360 DV的并行验证。这意味着尽管验证器并行工作,但不支持多个断言的并行运行(set_ check_option -local_processes)。也不支持通过网络进行证明分布(set_ check_option -parallel network)。这些选项被接受但被忽略。此外,Windows版本不支持GUI中的HTML选项卡。对于生成HTML输出的应用程序,如quantify或visualize_fsm,需要一个外部浏览器。

▷ 由于Windows平台上不存在Verdi™,因此Windows版本不支持在Verdi中进行调试或从FSDB读取初始状态。

▷ 如想要在Windows上验证SystemC,需进行64位Cygwin的最新版本安装。此外,软件包mingw64-x86_64-gcc-g ++必须安装在7.4.0版本中。

▷ 如在Linux系统上验证SystemC,必须安装软件包libstdc +±devel。

-版权所有,抄袭必究-

更多信息:http://www.softtest.cn/