装备电子系统的研发、测试、保障解决方案中心

形式化验证DV Verify
产品中心 形式化验证DV Verify
产品概述

FPGA设计越来越复杂,成本越来越高,尽早发现错误能降低风险,但传统的FPGA功能验证周期过长,且功能仿真很难达到100%覆盖率,故障分析效率很低,此外,编写大量的测试用例也会耗费大量的时间,因此,传统的功能验证已经难以满足现在的设计。

现在一般会使用形式化验证工具作为替代,形式化验证就是从数学算法上完备地证明设计功能的正确性,能实现功能验证的快速覆盖,再针对未覆盖的特殊功能编写测试用例,进行完善测试,它的主要优点是完备性,能够快速的达到一定程度的验证覆盖。

DV Verify采用形式化方式对FPGA设计进行功能验证,包含代码缺陷自动检查功能,能够自动生成与代码结构和安全性相关的功能断言,快速发现如数组越界等代码缺陷,它提供形式化分析引擎,可以对自定义功能断言进行验证,并提供覆盖率度量分析。

DV Verify包含DV Inspect,属性检查,覆盖率检查和故障注入四个部分,DV Inspect用于快速发现模块中的错误,属性检查运用断言进行属性检查,覆盖率检查提供特有的覆盖率驱动的验证,故障注入则能模拟各种故障场景。


图片1.png

DV Verify工作流程


功能特性

DV Inspect主要用于快速发现模块中的错误,能够在设计送入综合器编译之前执行功能验证,检查的效率很高且检查的种类很多。这个工具能够进行结构检查、安全性检查和激活检查。


图片4.png

DV Inspect工作流程


结构检查

结构检查能快速进行RTL代码的语法和语义分析,还可以在GUI中对两次的检查结果进行比对,发现改动后检查结果的不同,便于快速定位错误原因。


安全性检查

安全性检查包括以下检查内容:

图片3.png

安全性检查的内容


激活检查

激活检查包括无效代码检查、FSM检查和翻转检查。

无效代码检查以输入源码的各个分支为目标,检查这些分支条件是否都被执行。包括if-then-else和switch条件,以及default都会分析,对避免没有考虑的条件特别有用,通过x赋值,还能检查仿真和综合结果不匹配的情况。

状态机的检查主要是检查状态机中没有死循环的存在,检查状态机在复位时是否正确回到初始状态。工具自动识别源码中的状态机,对发现多个状态机间的错误内部连锁条件十分有用。

翻转检查主要是分析信号的开关能力。这项检查依赖于信号类型。例如如果信号是布尔型,工具就要检查它是否能从0变为1,从1变为0。

 

属性检查

这个功能就是通过编写功能断言进行属性验证,可以在没有Testbench的条件下开始验证设计,支持标准的基于断言的验证形式验证流程。它支持的断言语言包括:SVA、PSL和OVL。

属性检查具有独特结构的断言调试器,波形调试中使用不同颜色区分被测信号,指向故障原因,以及带有活动值注释和主动驱动程序跟踪的源代码分析。在断言开发过程中最常见且最耗时的其中一个步骤中,工具提供这种集成且高度直观的调试环境使工程师能够大大加快调试周期。

图片2.png

属性检查工作流程


覆盖率检查

覆盖率检查提供特有的覆盖率驱动的验证,它可以对形式化验证过程进行定量分析,与仿真覆盖度量合并,提供必要的覆盖度量来确认安全关键功能的彻底验证,评估验证进展并确定仍有待完成的工作,而验证中的间隙可以被自动标注在验证计划上,并用不同的颜色标注起来,表明不同的覆盖程度,覆盖率报告能够导出为UCDB格式,可以和仿真中产生的覆盖率报告进行合并。

Quantify可以将仿真结构覆盖衡量测试平台和测试套件对设计的覆盖程度,以及基于模型的变异覆盖衡量断言对设计的覆盖程度,这两个指标集成到单个覆盖视图中。此外,工程师还可以编写验证计划,以表明哪些目标将通过仿真、上板仿真和形式化工具来实现。可以将结果集成并注释回计划,包括唯一的形式度量,如有界的和完整的证明。


故障注入

形式化故障注入测试系统(FIA)能够简单灵活地自动模拟各种故障场景,从应被视为故障注入候选的信号开始,无需更改设计或执行代码检测步骤,提高对设计行为破坏的可见性,加快对失败断言的分析,消除了对特殊验证流或环境的需求,减少了工程工作。工程师可以从预先定义的库中选择或自定义故障模式,通常情况下,场景包含了位级故障位置、故障注入时间和故障类型的大量组合。

图片1.png

                故障注入系统工作流程