第2章 VC Formal工具套件与验证流程：核心概念、原理机制、实战要点
2.1 问题背景
随着设计规模和数据通路复杂度上升，传统仿真验证面临两个难题：一是测试向量难以覆盖深度状态空间；二是覆盖率收敛周期过长。VC Formal 作为 Synopsys 形式化验证平台，通过数学推理取代向量采样，在断言验证、数据通路验证和协议验证中扮演关键角色。
工程观察：很多团队引入 VC Formal 时，将形式化验证等同于“跑一条命令”，结果在断言质量、约束环境和收敛管理上遇到困难。形式化验证能力不仅来自工具，更取决于工具链的合理组合与流程纪律。
2.2 核心概念
- VC Formal：Synopsys 形式化验证平台，集成静态形式化验证（Static）、动态形式化验证（Dynamic）与应用级验证套件（Apps）。
- 属性 / 断言（SVA）：对设计行为的数学描述，是形式化验证的输入核心。
- BMC（有界模型检查）：在有限时间步内搜索违反属性的反例。
- 全证明（Full Proof）：在可达状态空间中证明属性对所有路径成立。
- 形式化覆盖率（Formal Coverage）：衡量属性检查对状态空间与逻辑行为的覆盖程度，指导收敛与签核。
2.3 原理机制
VC Formal 底层融合 SAT、BDD、SMT 等数学引擎，通过约束传播、状态抽象和位级推理，将 RTL 与断言转换为可判定的逻辑问题。
- 状态空间搜索：与传统仿真不同，VC Formal 在给定边界内遍历所有可能的输入序列，而非采样若干向量。
- 反例（CEX）：命中属性失败时，自动生成可仿真的波形 / 时序图，帮助定位根因。
- 证明与收敛：采用归纳法、抽象精化等技术，在资源限制下从“BMC 有界证明”向“全证明”收敛。
- 约束求解：将
assume、constraint与环境模型转换为求解器输入，保证验证状态合法可达。
2.4 流程步骤
- 属性与约束准备：梳理设计规格，编写 SVA 断言和形式化约束（assume / environment）。
- 工程配置与编译：使用 VC Formal 创建工程、读入 RTL、elaborate 顶层设计。
- 验证任务执行：按目标选择引擎，运行 BMC、全证明或 VC Formal Apps。
- 结果分析：区分证明（Proven）、反例（Failing / CEX）、未收敛（Inconclusive）三类状态。
- 覆盖收敛与回归：检查 Metric 覆盖率，补充断言或约束，将任务纳入 CI 回归。
# VC Formal TCL 脚本示例
create_project -name fifo_fv -dir ./work
read_file -format sverilog ./rtl/fifo.sv
elaborate -top fifo
# 读入断言
read_file -format sverilog ./tb/fifo_fv_props.sv
# 设置时钟与复位
create_clock -name clk -period 10 clk
set_constant rst_n 1
# 运行 BMC 20 步
bmc -depth 20 -property fifo_props
# 运行全证明
prove -property fifo_props
# 输出报告
report -summary建议：项目初期先选 1~2 个核心模块建立完整的属性环境并跑通，再横向推广到其他模块，避免团队在流程未定型时大规模铺开。
2.5 案例说明
案例：FIFO 满信号与写使能的冲突检测
假设 FIFO 深度为 8，断言为：
assert property @(posedge clk) !(full && wr_en);在 VC Formal 中运行 BMC 深度 8，立刻得到反例：FIFO 在连续写入 7 个周期后，第 8 个周期 full 拉高且 wr_en 仍为 1。通过波形定位，根因是指挥逻辑未在 full 时关闭写使能。修复后运行 prove，属性结果变为 Proven。
启示：BMC 适合快速找反例，全证明适合给出设计结论，两者需配合使用。
2.6 工具套件组成与流程总结
| 工具 / 模块 | 核心作用 | 适用场景 |
|---|---|---|
| VC Formal Static | 属性证明、BMC、全证明 | 控制逻辑、数据通路、协议检查 |
| VC Formal Dynamic | 动态形式化与仿真融合 | 复杂 SoC 系统级验证 |
| VC Formal Apps | 预置协议验证套件 | AMBA、PCIe、DDR、USB 等 |
| VC Formal DPV | 数据通路形式化验证 | 算术单元、流水线、ALU |
| VC Formal Metric | 覆盖率与收敛分析 | 验证进度评估、签核检查 |
2.7 误区提醒
- 误区 1：把 BMC 结果当作全证明。BMC 只在有限深度内有效，深度不足会漏掉深层错误。
- 误区 2：断言越多越好。错误或冗余的断言会拖慢引擎，并产生大量无效反例。
- 误区 3：忽略约束环境。没有合理的
assume，引擎会进入非法状态，验证结果不可信。 - 误区 4：只跑一次不管理资源。形式化验证需要按设计复杂度分层设置 timeout 和内存限制。
- 误区 5：不上回归。形式化任务应与仿真一样纳入每日回归，防止 RTL 修改破坏已证明属性。
2.8 实践清单
- ☐ 搭建 VC Formal 运行环境，确认 License 与 TCL 脚本通路正常。
- ☐ 为设计关键控制点编写至少 3~5 条 SVA 断言，并设置合法的
assume约束。 - ☐ 使用
create_project建立工程，读入 RTL 并完成elaborate。 - ☐ 先用 BMC 快速找反例，再对稳定属性执行
prove全证明。 - ☐ 收集并查看形式化覆盖率报告，针对未覆盖点补充断言。
- ☐ 将证明任务封装为 TCL 脚本，接入回归流水线。