企业官网建设流程全解析

formal验证是什么？

使用数学证明，不靠仿真激励，穷尽合法输入空间来证明属性 (Assertion) 永远成立。

formal验证的优势是什么？

用来弥补仿真覆盖率缺口。

什么样的场景适合用formal验证？

适合数据通路协议 ，FSM 状态机、控制逻辑、仲裁器、队列、握手协议 (AXI/APB)、计数器、数据校验、状态跳转、安全逻辑、复位逻辑，中等规模模块，建议模块层级，不要直接丢整个 SoC，大模块做切分，分块 Formal，把 RAM/ROM 做抽象模型。

用formal验证有哪些注意的地方？

三种A要怎么写。

1. assume：假设，约束输入，告诉工具哪些输入是合法的，不会去验证 assume；约束输入空间。
2. assert：断言，需要工具必须证明永远成立；失败给出反例波形。坏事情一定不能发生（safety），好事情必然发生（liveness）。
3. cover：覆盖点，证明存在某种场景可以发生，看场景可达性，关心的场景一定会发生。

将SVA与RTL联系起来有哪两种方式？

1.bind方式。

bind dut_module dut_sva u_dut_sva(.*);

优势：不污染rtl运行。可以复用sva文件。

2.include方式。

DUT 内部直接 include SVA；不推荐，污染 RTL 代码。

formal验证环境的准备步骤。

1.待测的rtl以及周围隔离的抽象model，裁剪无关的逻辑。

2.编写sva属性库。（assume/assert/cover）。

assume：做合法性约束。约束时序，复位，合法取值，握手时序，协议规则等。

3.formal验证环境列表和编译配置

文件列表包含：

1. DUT RTL
2. SVA property 文件（.sv，包含 assume/assert/cover）
3. 抽象模型 abs model
4. Formal 专用编译指令，排除仿真代码

jaspergold指令：

• blackbox：黑盒某些子模块，不展开内部状态，抑制状态爆炸；
• abstract：对存储、寄存器做抽象；
• cutpoint：切断部分信号传播边界，做边界抽象；
• bound：设置证明深度，有界模型检查 BMC；BMC（有界模型检查）：只证明 N 个时钟周期内属性成立； Prove：无界证明，证明永远成立；算力消耗远大于 BMC。

formal环境运行结果有哪些，怎么分析？

proved：属性被证明永远成立。

Falsified：找到反例 Counterexample；工具输出波形，复现 bug；看波形来区分是 RTL bug还是 assume 写的不合理，还是 assert 写的不对。修改 RTL / 修改 SVA 属性，重新跑 prove。

Undetermined：状态爆炸，算力耗尽，无法得出结论；需要做抽象、cutpoint、分块。

Vacuous（空洞 pass）：assume 约束太强，条件永远不会触发，assert 空洞通过，伪通过，高危坑。空洞检查是 Formal 环境必做检查！一定要看 cover 点是否可达。

formal验证如何sign-off？

• 所有关键 Safety 属性 Proved；
• 关键 Cover 点全部可达，无大量 vacuous 空洞；
• Undetermined 的属性做抽象优化，或者退而求其次 BMC 有界证明；
• 输出 Formal 报告，记录 cutpoint、blackbox、抽象假设。

formal验证过程中有哪些坑?

1.Assume约束错误, 过度约束，屏蔽 bug，assert 全部 pass，实际 RTL 有 bug。用 cover 点校验场景可达性，达到双重保障。

2.Vacuous 空洞通过，条件永远不成立，断言 “假的成立”。工具一般有选项打开空洞报告。

3.状态爆炸 State Explosion。大 FIFO、RAM、大量寄存器、复杂乘法，状态空间爆炸，全部 Undetermined。模块切分，分块 Formal；RAM 抽象、blackbox；cutpoint 切断信号路径；使用 BMC 有界证明替代无界 prove；

4.复位处理不当，SVA 必须加disable iff(!rst_n)，否则复位阶段报虚假 falsified

5.Liveness 活性属性证明失败。活性属性证明开销高，很多时候需要额外 fairness assume（公平假设，比如输入不会永远 hold valid）。

6.仿真与 Formal 两套 SVA，维护成本高。使用同一套 SVA，既可以 UVM 仿真跑断言，也可以 Formal 证明。

7.Formal 报反例，是不是一定 RTL 有 bug？仅说明在当前 assume 约束集合下，property 不成立。排查顺序：

1. 反例的输入激励现实不会出现 →assume 约束问题
2. 激励合法，RTL 行为符合 spec，但断言报错 →property 属性 bug
3. 激励合法，RTL 行为违反 spec →RTL bug

配合jaspergold使用：

1. 使用visualize打开 counterexample 波形，重点看：输入信号、property 内部子表达式哪里不满足。
2. 可以临时 disable 这条 assert，单独检查中间信号行为，看 DUT 实际输出是否符合 spec。
3. 将 counterexample 导出激励，在仿真环境回放，如果仿真同样报错，大概率 RTL 问题；仿真跑出来正常，大概率 formal 约束 /property 问题。

formal验证举例：

最近想总结一下看过的代码，如有错误，欢迎指正。我们从top文件开始看起。

top module里总是有dut的例化以及dut和env的连接. 这点跟simulation验证平台一样。

formal验证平台的pkg.sv文件包着所有的有关enum和type的定义也可以被其他文件以import pkg::*的方式使用，simulation的验证平台是包了所有的验证平台下的文件以及引用的文件，使用方式相同。

formal验证平台的env里，有clock，reset的处理以及做的假设（assume)，interface的例化。agent和scoreboard的例化（做补充检查）。自己写的做逻辑判断的cover property，assert property, assume property。

设计数据流动的文件， master agent来驱动数据流到interface，slave agent来监控interface的数据流。agent是经过vip例化出来的。

parameter确定好后被放在define文件里。

编辑japergold 适用的tcl文件，里面有一些常规命令还有自己添加的assume假设（assert和 cover应该也可以)。

最后由makefile来确定整个验证平台怎么跑。确定好工作路径之后，首先vcs编译pass。其次启动jaspergold运行命令。

jg -fpv *.tcl

这是一个仅用sv搭建的环境，还没见过uvm的formal验证环境，有机会补充一下。

此环境是使用Cadence JasperGold工具来做formal验证，也可以使用Synopsys VC‑Formal来做验证。