形式验证替代仿真的决策依据与工具操作对比

在大规模数字IC验证中，形式验证（Formal Verification, FV）——尤其是属性检查（Property Checking / Model Checking）——能对指定性质做数学穷举证明，弥补仿真只覆盖部分向量的不足。但它不能完全替代仿真。本文梳理何时可用FV替代/补充仿真，并以Synopsys VC Formal / Cadence JasperGold 为例说明操作差异。

一、形式验证能证明什么，不能做什么

能力 形式属性检查（ABC/Induction） 动态仿真（UVM）

覆盖度 数学穷举（无向量依赖） 仅受生成向量集限制

适合模块 控制单元、仲裁器、FIFO、总线桥、CRC checker 复杂datapath、视频编解码、系统级场景

发现未知X传播 可设assume约束排除非法X 需手动注入

运行时间 秒~分钟（小模块）；状态爆炸可能不收敛 小时~天（回归）

环境建模 需写assume约束（环境抽象） 需写Bus Functional Model / VIP

结论：FV适合无状态爆炸的小模块 + 关键控制逻辑做全证明；系统级复杂数据流仍以仿真为主。

二、决策依据：何时可用FV替代/前置仿真

1. 模块规模小（寄存器<500，FSM状态<50）且以控制为主

  → 可用FV完全替代单元级仿真（写SVA + prove）

2. 存在安全属性（如"Req→Grant必在N周期内"、"Ack不能连续两次无Req"）

  → FV可证明无违例；仿真仅能抽样验证

3. 需证明无死lock / 无非法状态可达

  → FV用 Induction 证明；仿真难遍历所有路径

4. 含深FIFO / 大乘法器 / 浮点 datapath

  → FV难收敛 → 保留仿真，FV仅验接口协议（Valid/Ready握手）

5. 认证要求（ISO 26262 ASIL D）

  → 推荐FV做Structural/Control证明 + 仿真做Function覆盖，互为补充

三、Synopsys VC Formal 操作要点（SVA Based）

3.1 准备

• RTL + SVA断言（assert property / assume property / restrict property）

• blackbox 未实现模块或ROM

- Clock/Reset定义：

set_design -clk clock -rst reset_n -rst_active low

3.2 运行属性检查

# 读设计

read_rtl -verilog rtl/*.v

read_sva -file assertions.sva

# 设置约束（例：输入data稳定2周期）

assume -expr {stable_data == 1'b1}

# 证明所有assert

prove -all

结果解读：

• Proven：数学上永不为假（在该抽象层）

• Falsified：找到Counterexample → 回RTL查bug

• Inconclusive (Bounded)：证明到第N层（可加大depth或加Lemma）

3.3 覆盖与CEX调试

show_cex -assert <id>   # 波形形式查看反例

report_prove -summary

四、Cadence JasperGold 操作对比

JasperGold 使用 ProofGrid + Visualizer：

# 设置顶层与文件

set_top dut_top

read_verilog rtl/*.v

read_sva assertions.sva

# 证明

prove -task prove_all

# 查看交互

gui_open

主要差异点：

项目 VC Formal JasperGold

证明引擎 ABC + proprietary ABC + IC3 enhanced

交互调试 CEX波形文本/波形 Visualizer GUI（状态机图、Cone of Influence）

抽象/lemma管理 set_lemmas save_lemmas / restore_lemmas

常见扩展 支持CRV(COI Reduction) 内置 Security / Connectivity Apps

两者均要求 SVA断言 + assume约束正确——垃圾约束入，垃圾证明出（GIGO）。

五、形式验证常见坑

1. Over-constrain（assume太强）：证明通过但实际环境不满足assume → 假安全  

  → 用 cover property(assume_conjunction) 确认环境可激活

2. Under-constrain（未assume X-free输入）：工具可能用X推导使assert trivially pass  

  → 加 assume property (~$isunknown(sig))

3. 忽略Black box输出约束：Black box输出需assume合理范围，否则证明无意义

4. 把Datapath复杂运算当prove目标：建议拆为接口协议FV + 定向随机仿真验运算

六、结语

形式验证不是仿真的全盘替代，而是控制逻辑完备性证明 + 仿真盲点补充。决策准则是：小控制块 → FV全证明；大Datapath → FV验接口协议 + 仿真验功能 + 覆盖率。掌握VC Formal / JasperGold中SVA编写、assume/assert平衡与Counterexample分析，方能让形式验证真正提升签核信心。