Onespin为德国一家专业致力于高安全性可编程逻辑解决方案的公司，是形式化验证技术的领导者。针对FPGA/CPLD，公司有一系列的产品來保障质量。

一、RTL缺陷检查及覆盖率测试工具360DV-Inspect

FPGA的开发和测试过程中，对RTL代码中存在的低级缺陷（如死代码、数组越界、除零、数据值范围越界、FSM状态机中的不可达状态及不可达转移等等）的精确检查是特别重要的一环。低级缺陷一般隐藏很深，这类错误是直接影响预期逻辑功能或数值计算功能的正常实现，并且通过人工评审、常规编码规则检查、功能仿真等手段很难发现和定位。这类缺陷的精确和完善的检出需要采用先进的形式化分析技术，这种技术可以考虑所有的输入组合以及对代码的每条路径下的各个信号变换进行计算，从而精确检出存在于代码中的特定路径下低级错误，并且可以将这条路径显示出来以便于设计/测试人员快速理解/修改问题。

Onespin:a Siemens Business的RTL缺陷检查及覆盖率测试工具360DV-Inspect能自动精确检测出RTL代码中的低级缺陷并定位到相应的引发错误的RTL代码序列以便于功能仿真之前即可修正低级错误；自动分析出死代码、不可达条件、不可达FSM状态、不可达FSM转移，对于可达的代码部分能自动生成测试用例序列证明其可达性，包括语句覆盖、分支覆盖、翻转覆盖、状态机覆盖。

二、逻辑等效性验证工具360EC-FPGA

在高可靠行业如核电、航空航天中通常都会要求对FPGA系统做逻辑等效性检查。综合工具及布局布线工具有可能会在综合过程中引入未知的错误和漏洞而导致系统的故障。这就需要相应验证工作的开展来确保RTL与综合后网表的逻辑功能一致性、综合后网表与布局布线后网表的逻辑功能一致性、RTL代码与布局布线后网表间的逻辑功能一致性。

Onespin:a Siemens Business的逻辑等效性验证工具360EC-FPGA能够开展以上的工作，特点如下：

支持验证RTL代码与综合优化后的网表间的功能一致性

支持验证综合优化后的网表与布局布线优化后的网表间的功能一致性

支持验证RTL代码与布局布线优化后的网表间的功能一致性

支持对组合电路、时序电路及混合电路的一致性验证

提供调试器来生成反例并以波形图和代码活动图的方式联合展示不一致的具体原因及信号路径

自动识别分析FPGA芯片中的各种特定硬件原语行为

自动分析匹配RTL与网表中的输入\输出\内部信号

支持多种HDL语言以及混合语言模式设计

自动分析匹配RTL与网表中的时钟\门控时钟、同步\异步复位信号

自动分析匹配RTL与网表中的FSM状态机

能够全自动匹配RTL与网表中的各逻辑等效子结构、内部等效信号、内部等效触发器

自动分析匹配RTL与网表中的未驱动端口\信号

自动分析匹配RTL与网表中的信号反馈路径以及锁存电路

自动分析匹配RTL与网表中的PLL核、DLL核、DCM核

自动分析匹配RTL与网表中的BLOCK RAM 核

自动分析匹配RTL与网表中的FIFO IP核

三、基于形式化方法的功能验证平台360DV-Verify

随着FPGA系统日趋复杂，仅通过人工设计用例和随机测试激励生成进行仿真是无法满足复杂FPGA系统的测试验证需求的。

Onespin:a Siemens Business的基于形式化方法的功能验证平台360DV-Verify是一个形式化方法的针对需求的功能验证平台，其特点如下：

◆ 支持Operational ABV验证方法学

◆ 支持对设计进行模块级功能验证

◆ 支持对设计进行多模块集成功能验证

◆ 支持对多种RTL设计语言的功能验证；

◆ 支持以SVA验证语言描述设计的高级\低级功能/时序需求

◆ 支持以ITL验证语言描述设计的高级\低级功能/时序需求

◆ 支持以TiDAL验证语言描述设计的高级\低级功能/时序需求

◆ 自动分析、生成具体测试用例序列以便于理解和修正不完整、有错误的功能/时序需求

◆ 自动验证RTL代码是否完整、正确地实现了各设计模块的所有功能/时序需求

◆ 自动分析、生成不满足特定功能/时序需求的具体测试用例序列以波形图以及RTL代码联动方式来理解和修正RTL模块设计

◆ 自动分析、生成满足特定功能/时序需求的具体测试用例序列以波形图以及RTL代码联动方式来证明具体功能/时序需求的正确性

◆ 提供精确到RTL代码行的详细验证报告指示功能需求集的测试验证程度