Dinglei_hello · 2021年12月21日

概述Formal verification

Formal verification的优势在哪里?

首先我们应该都有一个共识:

在数学上穷尽分析所有可能的RTL空间是最理想的验证结果,这也是传统的仿真很难做到的事情。

640.gif

FPV方法的优点包括:

做正确的验证

这句话可能比较哲学哈。

以一个工程师的角度,你是否问了自己很多次:我们应该如何正在验证我们的设计?

理想的方法是从数学上证明它们符合其规格。但不幸的是,由于工具的限制,我们大多基于仿真的方式来进行验证。这是工程中上市时间技术水平对我们的约束,

随着这些限制的减少,我们应该尽可能地摆脱这些旧的方法(仿真)或者尝试选择FPV方式进行一些验证。

完全覆盖

如果我们将“coverage”定义为我们对设计分析的空间与设计全空间的比值,FV本质上能够提供完全的覆盖。完全的FV对于大规模的设计是不太现实的,但是FV方法仍然能够达到非常多次仿真回归的效果。

最小的场景示例

大多数FV引擎能够产生最小的场景(RTL行为),这些数个周期内的行为可能要在数千个随机仿真环境中才能复现,这使得FV更容易定位问题。

边界场景(Corner Cases)

FV会遍历任何没有约束掉的行为,这意味着FV工具很容易发现有趣的Corner Cases(头脑风暴也很难想到的场景)。对这个场景进行分析,可以检查我们的EDA验证环境是否不够完备,是否在某个地方(激励、参考模型和检查机制)存在着过约。

基于State-Driven和Output-Driven的分析

FV可以cover设计内部的任何状态,设计可以根据这个cover分析产生这个状态的相关设计行为。仿真是激励驱动的,通常覆盖到某个特定的复杂设计场景都会比较困难。

证明永恒的问题(Infinite Behaviors )

如果使用仿真,你如何能够证明设计永远不会到达某些状态。用FV,数学的推理力量,我们就可以回答这个问题。

Formal Verification能用来做什么?

基于前文所述Formal Verification的优势,可以诞生多个FV的应用场景。

complete coverage,确保所有可能的场景都被覆盖到,以提高验证交付自信,防止出现Intel 奔腾FDIV bug等类型的问题。

bug hunting,当设计规模较大时,可以针对设计特定的风险区域进行更加全面的覆盖测试(注意,前提是无法做到Full proof,不然就没有bug hunting的必要了

design exploration,利用数学分析可以帮助我们更好地理解RTL行为。

FV FOR COMPLETE COVERAGE

为了进一步了解FV方法,先让我们花点时间来考虑一个简单的验证问题:

验证一个有两个32位输入的加法器。

image.png

为了充分验证该设计的所有可能的输入,我们需要仿真264种可能的组合。如果你有一个超快速的仿真器和服务器资源,可以每秒仿真214个周期(已经非常快了),这意味着它将花费你2*40秒(数万年)的时间来检查所有可能的值。

就算验证经理分给你这么久的时间,可能我们这颗蓝色星球也等不起你验完啊。而且,这仅仅只是测试了一拍的设计行为,还没有考虑时序场景。因此,基于完全覆盖这个需求,相比EDA仿真,FV是我们真正需要的。

01 TIP 1.1

当你想要获得设计行为的完全覆盖时,请考虑使用FV作为主要验证方法。

FV for Bug Hunting

对于一些规模比较大的设计,FV完全覆盖是不太可能的。这才有了EDA 仿真技术的用武之地啊~

当设计规模比较大,或者逻辑比较复杂时,无法做到Formal Full proof。在这些情况下,FV不能完全替换仿真。但这不意味,FV已经没有用了,FV仍然能够验证到比仿真方法多很多的设计状态。

因此,作为仿真的补充,FV仍然可以作为一种有价值的验证方法,否则可能会遗漏潜在bug。

01 TIP 1.2

当你有一个具有复杂逻辑的设计,无法做到Formal Proof时,可以考虑将Formal 作为仿真的补充。

FV for Exploring Designs

FV的另一个主要用途是作为探索RTL设计行为的工具。FV工具能够分析所有的设计空间,然后找出一个示例让设计查看特定的设计行为。

这可以看作是逆向仿真:当你不知道什么样的激励能够产生特定的场景,可以让FV跑出这个场景再去分析。例如,你希望覆盖输出32‘hffff_ffff,但是不知道应该输入什么样的激励,这时候FV可以帮到你。

有时候一个特定的输出是多个周期输入耦合作用的结果,可能只有FV能够找出一个精确的输入序列。

换句话说,使用FV用作设计探索时,我们只要指定的是目的地,而仿真需要你指定旅程中的每一个脚印。

01 TIP 1.3

你可以轻松地指定感兴趣的设计状态或输出,然后使用FV帮你找到特定的输入序列。

Formal Verification在真实项目中的应用

image.png
上图是SOC设计流程中Formal Verfication的一些应用,主要包括:

基于断言的验证(ABV)

如今断言已经非常广泛地应用到芯片研发流程中了,例如使用SVA来描述设计的属性(properties )。在某些情况下,仅仅使用属性也可以描述一个设计的全部规格。使用ABV并不意味着正在执行Formal Verification,因为断言也可以在仿真中进行检查。

事实上,在仿真中检查断言是断言的最主要应用。

Formal Property Verification (FPV)

这是指使用formal 工具来证明断言。FPV是一种非常通用的技术,可以进一步发展再细分为许多额外的技术:

2.1 Full Proof FPV。

这是经典的使用FPV来代替仿真,验证RTL是否正确地实现了规格。

2.2 Bug Hunting FPV。

这是指使用FPV来作为仿真的补充,在Formal无法彻底验证设计的情况下。它仍然是一种非常强大的验证手段,发现corner-case bug并覆盖比仿真更多的设计空间。

2.3 Unreachable Coverage Elimination。

如果你最主要的验证方法是仿真时,通常会在项目中会有一些代码覆盖率永远无法达到,需要验证团队弄清楚它们是否是dead code。FPV可以用来达到这个目的,方便代码覆盖率waive。

2.4 Specialized FPV Apps。

这是指适用于特定设计属性的FPV,如验证寄存器、状态机、连接等等,主要目的就是使用FPV提高某个特性的验证效率

Formal Equivalence Verification (FEV)

这是指使用formal 比较两个模型并确定它们是否等价的技术。比较的模型可能都是高级语言模型、RTL或网表等等。高级语言FEV可以比较C算法模型和Verilog,RTL2RTL、RTL2NETLIST、NETLIST2NETLIST在后端流程(例如ECO时)中用的比较多。

作者:验证哥布林
原文链接:https://mp.weixin.qq.com/s/gH0P9_dmuKdv91oEyI7JbQ
https://mp.weixin.qq.com/s/G_bSoe2-9qsU762noU7s4Q
https://mp.weixin.qq.com/s/xBWoRwKBbv7Z0QWxcGSjKg
微信公众号:
 title=

推荐阅读

更多IC设计技术干货请关注IC设计技术专栏
2 阅读 778
推荐阅读
0 条评论
关注数
8581
内容数
782
主要交流IC以及SoC设计流程相关的技术和知识
目录
极术微信服务号
关注极术微信号
实时接收点赞提醒和评论通知
安谋科技学堂公众号
关注安谋科技学堂
实时获取安谋科技及 Arm 教学资源
安谋科技招聘公众号
关注安谋科技招聘
实时获取安谋科技中国职位信息