第3章 形式化验证工程创建：核心概念、原理机制、实战要点

问题背景

形式化验证与动态仿真的核心差异在于：仿真通过激励驱动设计观察行为，形式化验证则通过数学推理穷尽状态空间。JasperGold工程创建是形式化验证的第一个关键环节，它决定了后续属性编写、约束注入、调试与收敛的效率。本章从“工程创建”出发，梳理JasperGold工程的核心概念、底层原理与实战操作路径。

大量初学者的常见问题是：把大部分精力花在SVA语法学习上，却忽略了工程环境搭建与设计/属性/约束三者之间的正确关联方式。一个不规范的工程，往往会导致属性读入失败、证明结果不可信或者调试周期大幅拉长。

核心概念

• JasperGold工程（Project）：用于管理设计文件、SVA属性、约束、证明任务和结果的工作单元，工程文件记录所有配置与命令历史。
• 设计读入（read_file）：将RTL或门级网表编译到工具内部的数据模型中。
• 属性（Property）：以SVA断言表达的设计待验证行为，是形式化证明的目标。
• 约束（Constraint）：通过 assume 或约束文件限制输入空间，帮助工具收敛于真实可达状态。
• 证明收敛（Proof Convergence）：工具遍历全部可达状态后给出“成立”或“不成立”的确定结论。
• Bounded / Unbounded Proof：有界证明是指在指定cycle数内未发现违反；无界证明是对所有时间步的完整证明。

工程创建流程框架

原理机制

JasperGold引擎将“设计 + SVA属性 + 约束”统一转换为时序逻辑数学模型，构建有限状态机状态转移关系。在求解阶段，工具通过 SAT/SMT 求解器对状态空间进行搜索，并采用 演算抽象 与 反例引导细化（CEGAR） 等策略缩小搜索范围，最终达成对属性的确定性结论。

流程步骤

1. 创建工程目录与工程文件：规划独立的工作目录，设置工程名。
2. 读入设计文件：使用 read_file 导入RTL/SV/门级网表，并指定顶层模块。
3. 设置当前设计：用 current_design 指定验证目标模块。
4. 读入SVA属性文件：加载断言与约束文件。
5. 运行证明：调用 prove 启动形式化分析。
6. 查看收敛状态：通过 verify_status 检查每个属性的证明结果。

典型JasperGold命令行过程如下：

# 启动JasperGold
jg

# 1. 创建工程
new_project -dir ./fpv_prj -name counter_fpv

# 2. 读入RTL设计
read_file -format sverilog -top counter_top ./rtl/counter_top.sv

# 3. 设置当前设计
current_design counter_top

# 4. 读入SVA属性文件
read_sva ./sva/counter_props.sva

# 5. 执行形式化证明
prove -property counter_top.p_count_4bit

# 6. 检查证明状态
verify_status -list

案例说明

以一个4位递增计数器为例，其RTL代码如下：

module counter_top(
  input logic clk,
  input logic rst_n,
  input logic inc,
  output logic [3:0] count
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) count <= '0;
    else if (inc) count <= count + 1'b1;
  end
endmodule

编写SVA属性文件 counter_props.sva：

// 属性1：count 始终在4位范围内（预期证明通过）
property p_count_4bit;
  @(posedge clk) disable iff(!rst_n)
  count inside {[0:15]};
endproperty
assert property (p_count_4bit);

// 属性2：count 永远不等于 4'b1111（预期证明失败）
property p_never_max;
  @(posedge clk) disable iff(!rst_n)
  count != 4'b1111;
endproperty
assert property (p_never_max);

运行 prove -property counter_top.p_count_4bit 会得到 Proof Passed；运行 prove -property counter_top.p_never_max 会得到 Proof Failed，并生成反例波形，反例中可观察到count从0递增至15后仍继续计数并回卷。

表格总结：工程创建关键阶段

阶段	核心任务	输入	输出	常用命令
工程初始化	创建工程目录与配置文件	工程名 / 路径	工程文件	new_project
设计读入	将RTL/门级网表导入工具	RTL / SV文件	编译后的设计模型	read_file, current_design
属性导入	加载SVA断言与约束	.sva 属性文件	属性集合	read_sva
证明执行	运行形式化分析	属性 + 设计 + 约束	证明结果 / 反例	prove
结果分析	审查收敛状态与反例波形	证明结果	收敛报告 / Counterexample	verify_status, visualize

误区提醒

实践清单