coverage type

formal和simulation一样，也是基于coverage-driven的验证方式；针对formal的coverage metrics，可以分为以下几种（不同工具定义略有不同，本文以Jaspergold为例）：

code coverage
code coverage分为branch，statement，expression，toggle；这部分概念和simulation类似，如下图：

用于衡量cover item(CI) (CI可以简单理解为RTL code)在验证过程中是否被覆盖到；因为formal是工具自动施加激励，CI的覆盖结果分为以下几种：
Covered：工具追踪并覆盖了该CI
Uncovered：在有限的时间内，未追踪覆盖该CI
Unreachable：在给定的约束条件下，无法覆盖该CI（可能存在over-constraint的问题）
Dead-code：在任何条件下，都无法覆盖该CI

functional coverage
functional coverage：和simulation一样，通过自定义covergroup的方式收集功能覆盖率。
一般formal验证中，更多的是使用SVA, PSL, TCL cover properties的方式来收集感兴趣的场景（meaningful scenarios）；

上述的code coverage，functional coverage可以合并称作Stimuli Coverage

checker coverage
Stimuli Coverage达到100%，并不能表明验证的完备性，只能说明当前formal平台下激励足够充分，各类CI都覆盖到；但是RTL的正确性，需要assertion作为checker来保证；需要引入checker coverage，checker coverage分为COI coverage和 Proof Core两种：

COI coverage
COI(CONES OF INFLUENCE): 逻辑锥的含义，是Formal工具对property的逻辑电路映射；覆盖结果如下：
Checked：该CI和某个/某些assert相关联；
Undetectable：该CI和任何assert都没有关联，也就说CI改变或者去除，不会引起任何asstertion fail。

Proof Core
proof core是对逻辑电路更精确地划分，是COI的子集：

如下图，一个简单的assertion（ asster $onthot0(B)）从COI的角度看，涉及很多逻辑单元；仅通过这一个asstertion无法保证前面运算单元的正确性，这部分逻辑对于Proof Core是Unchecked的。

通过分析Proof Core，增加额外条件，提高assertion的完备性，如下：

Proof Core的覆盖结果如下：
Checked：该CI可以被工具分析的assertion检查到。
Unchecked：该CI不可以被工具分析的assertion检查到。

Proof Core的精确度可以配置为Normal Precision(flop-level,default)和High Precision（code-level）两种。

Mutation：是一种更为精确地对checker完备性检查的方式，可以理解为对RTL code 注错。随机对RTL注错，例如对某些逻辑取反，查看assertion是否fail。如果assertion足够完备，RTL的任何注错，都会引起assertion fail。此时assertion相当对RTL的 1:1 实现。

衡量的精度越高，需要的努力也越大；一般首先保证COI达标，再考虑Proof Core；综合考虑ROI，建议对一些generic module的验证，采用mutation sign-off；对于Unite Level Module，通常不会使用mutation。

在VC fomal中，称作Formal Core；在Jaspergold中，称作Proof Core。

上述的stimuli coverage，checker coverage可以合并称作Formal Coverage

bounded coverage
bounded coverage是用于评估当前proof depth是否足够作为sign-off标准，可以参考上篇bounded proof的内容。

Coverage Methodology的总结如下：

Note: 因为formal环境中的辅助代码都是可综合的代码风格，所以覆盖率包含DUT和formal环境两部分。这一点formal和simulation不同

sign-off flow

以覆盖率作为sign-off的标准，各家工具略有不同，但大体一致：
Jaspergold建议如下：

VC Formal建议如下：

大致步骤总结如下

排除formal平台(没有underconstraint和overconstraint)和DUT(没有deadcode)的基本问题；
首先分析COI覆盖率，补充缺失断言，COI达到100%；接着分析Proof Core，补充缺失断言，Proof Core达到100%。（未覆盖部分的wavie需要review并comment）
对于inconclusive assertion，需要确认当前的cycle depth是否充分；
预期的function cover被覆盖；
针对某些模块，需要进一步的mutations或者FTA (Formal Testbench Analyzer)分析处理；
在回归阶段，部署相关的Deep Bug Hunting策略；

理想的Sign-off目标如下：

所有的covers/vacuity-checks都被覆盖，未被覆盖存在合理的解释；
没有CEX遗留，所有的assertions都是full-proof或者bouned-proof的状态；
COI达到100%
Proof Core达到100%
通过mutations的注错测试

上述内容针对只使用Formal Sign-off的Block Level DUT；如果DUT使用Formal+Simualtion两种验证方式或者使用Formal做System level的验证，上述内容需要做相应的修改；同一家的工具支持Formal和Simualtion的覆盖率merge；

sign-off flow不单单是覆盖率的收集和分析，涉及验证流程的方方面面；包括但不限于Design SPEC是否对formal的部署友好，Formal Verification Plan的制定，Formal/Simulation Co-Verification，来自Formal Expert的review，Formal TB的搭建，覆盖率的收敛，dashboard/trend chart，回归策略和DBH，Checklist的确认，Sign-off，ROI评估，lesson learn 等。

sign-off flow相关的paper：

FV Signoff in the context of Mainstream Formal Verification (JUG 2022 Recording)

A Coverage-Driven Formal Methodology for Verification Sign-off

Formal Verification (五) coverage、sign-off flow相关推荐

阅读论文Formal verification of smart contracts based on users and blockchain behaviors models
1 题目(Formal verification of smart contracts based on users and blockchain behaviors models) 1.1 作者.出 ...
Formal Verification (一) 形式验证的分类、发展、适用场景
资料分享:百度网盘提取码:csdn Definition Formal Verification:利用数学分析的方法,通过算法引擎建立模型,对待测设计的状态空间进行穷尽分析的验证. Kinds of ...
Formal Verification (二) FPV、APPs
通过上一篇对Formal Verification有了基本的认识:本篇将通过一个简单的例子,感受一下Formal的"魅力":目前Formal Tool主流的有Synopsys的VC ...
linux内核形式化验证,说说形式化验证（Formal Verification）吧
原标题:说说形式化验证(Formal Verification)吧前言:被@暴走恭亲王点名,不得不写这个小文,笔者学识浅薄,而形式化验证这个题目不但大,而且深,笔者掌握的数学知识在专业人士里也就是幼 ...
Formal Verification of Smart Contracts Short Paper
Formal Verification of Smart Contracts: Short Paper ABSTRACT 提出将使用F*框架用于编写代码 1. INTRODUCTION 本文目的:通过 ...
Formal verification (FV) 处理复杂度形式验证第10章
目录一.设计状态和相关复杂性二.内存控制器三.观察复杂性问题四.简单的收敛技巧 1.选择正确的战斗 2.引擎调整 3.黑盒(blackboxing) 4.参数和尺寸缩减 5.案例分解 6.属性 ...
formal Verification 形式验证形式验证的最大障碍：误报（false positives）的危险第9章
目录一.SVA语言的误用 1.缺少分号 2.双时钟边沿的断言 3.带断言的短路函数 4.信号采样的细微影响 5.不活跃的活性属性 6.预防SVA相关假阳性二.真空问题 1.重置错误的误导覆盖点 2 ...
Formal Verification (四) bounded proof、bug hunting、advanced topic
bounded proof 形式验证本质上是一种model checking:不同类型的模型检查,调用不同的算法引擎:对于特定的属性求解,需要调用合适的engine:symbolic model ch ...
uvm 形式验证_谈一谈IC flow中的形式验证
By definition, formal verification is the use of tools that mathematically analyze the space of poss ...

Formal Verification (五) coverage、sign-off flow

coverage type

sign-off flow

Formal Verification (五) coverage、sign-off flow相关推荐

最新文章

热门文章