Synopsys VC Formal形式化验证入门到精通 - 第3节

问题背景：形式化验证的门槛与破局点

形式化验证不是把代码“跑”起来，而是把代码“证”出来。与仿真不同，VC Formal 并不依赖测试向量，而是通过数学引擎穷举所有状态。但这也带来明显的工程门槛：如何组织工程目录、配置工具链、声明时钟复位、导入 RTL 与属性，直接决定验证效率与能否收敛。

很多新用户面对 vcformal 命令行或 Desktop GUI 的第一反应是：从哪里开始？本章即解决三个问题：工程长什么样、工具如何调用、属性如何跑通。

核心概念：VC Formal 工程环境四块基石

搭建 VC Formal 工程，本质上是在管理以下四类对象：

• 工程空间（Work Space）：存放编译产物、日志、报告与中间数据库的目录；分布式或回归环境下必须可复制、可迁移。
• 设计输入（Design Input）：RTL 文件、网表、UPF 功耗描述、SDC 约束；VC Formal 会将它们编译为统一的内部形式化模型。
• 验证意图（Verification Intent）：SVA 属性（Property）、约束（Constraint）、覆盖点；这是形式化验证的核心，区别于仿真的“激励生成”。
• 运行引擎（Engine）：Proof Compiler 负责解析与编译，形式化求解引擎负责证明或找反例，DPV 专门处理数据通路运算。

原理机制：从 RTL 到可证明属性

VC Formal 的编译流水线分为四个阶段：

1. 解析与 Elaboration：读取 RTL 和 SVA 文件，完成设计层次展开、参数例化、时钟推导和信号连接。
2. 形式化建模：将电路映射为安全状态机与转移关系，组合逻辑被编码为布尔公式。
3. 属性编译：将 assert、assume、cover 转换为时序逻辑表达式，附加到模型中。
4. 引擎求解：由 SAT/BDD 引擎对每个属性执行可达性分析。若所有反例路径均不可达，则证明；若存在可达反例路径，则报告 counterexample。

流程步骤：从零搭建可运行工程

以命令行方式搭建一个最小工程，推荐采用以下六步：

1. 创建工程目录：work 目录专门存放编译产物。
2. 设置环境变量：配置 VCFORMAL_HOME 与 PATH。
3. 准备文件清单：编写 filelist.f，列出全部 RTL 设计与 SVA 文件。
4. 启动 VC Formal Shell：进入交互式 Tcl 环境 vcformal。
5. 读取与细化：read_file 加载设计，elaborate 指定顶层模块。
6. 声明时钟复位，运行证明：配置时钟与复位后，即可执行证明任务。

# 步骤1 : 创建目录
mkdir -p ./vc_proj/work

# 步骤2 : 配置环境
setenv VCFORMAL_HOME /opt/synopsys/vcformal_2023.03
setenv PATH ${VCFORMAL_HOME}/bin:${PATH}

# 步骤3 : 编写 filelist.f
# 接着启动交互式工具
vcformal

在 VC Formal Shell 中执行 Tcl 命令：

set work ./vc_proj/work
read_file -format sverilog -vcs "-f ./filelist.f"
elaborate -top counter

clock -domain clk -period 10
reset -signal rst_n -active low

assert -type property -file ./props/prop1.sva
prove -property p_reset

案例说明：轻量级计数器验证

以一个带同步复位的 4 bit 计数器为例：

// counter.sv
module counter(
  input logic clk,
  input logic rst_n,
  output logic [3:0] q
);
  always_ff @(posedge clk) begin
    if (!rst_n) q <= 4'h0;
    else        q <= q + 1'b1;
  end
endmodule

对应的 SVA 属性文件：

// prop1.sva
property p_reset;
  @(posedge clk) !rst_n |-> ##1 q == 4'h0;
endproperty
assert property(p_reset);

执行 prove -property p_reset 后，工具会尝试证明：rst_n 为低电平的下一拍，q 必定为 0。若反例存在，会输出 VCD 波形可导入 Verdi 查看。

进一步，如果写出错误属性 !rst_n |-> ##2 q == 3，工具会返回 counterexample，并指明 q 实际取值为 0——这正是形式化验证的“犀利之处”，也是逆向检查的好方法。

表格总结：关键配置项速查

误区提醒：新手最常见的五个偏差

• 把属性当激励：从仿真思维出发编写 SVA，忽略了形式化引擎需要的是“断言”，不是“观测”。
• 不设约束：场景是不完整的状态空间，必须通过 assume 限制输入序列，否则证明会因模型过强而失败。
• 忽略编译警告：Elaboration 阶段的 warning 往往暗示信号悬空、切片越界或异步逻辑建模错误。
• 一次 prove -all：在工程初始化阶段属性尚未成熟，批量证明导致大量超时，难以定位瓶颈。
• 不归档 counterexample：反例波形是最有价值的调试资产，应自动归档到指定目录并纳管。

实践清单：本章动手任务

• 安装并配置 VCFORMAL_HOME，验证 vcformal 命令可启动。
• 建立 vc_proj 工程目录，包含 work、rtl、props、logs 四个子目录。
• 编写一个不超过 30 行的 RTL 模块（如移位寄存器或计数器）。
• 使用 read_file 加载设计，elaborate -top 建立顶层模型。
• 声明 clock 与 reset，确认 report -clock 能看到时钟域。
• 编写一条 SVA 断言，覆盖复位后时序行为。
• 运行 prove -property，查看 Proof 状态为 proven 或 counterexample。
• 故意将属性写错一次，触发反例，并用波形工具打开 VCD，确认失败原因。