第1章 形式化验证与Cadence JasperGold概览：核心概念、原理机制、实战要点

1.1 问题背景：仿真验证的“视野盲区”

在大型 SoC 与 IP 验证中，动态仿真通常占据验证周期的大部分时间，但仿真本质上只能证明“被跑到的那几条路径没有发现错误”。随着状态空间膨胀，组合爆炸使关键 bug 更容易隐藏在仿真无法覆盖的边界中。

• 覆盖率盲区：随机测试难以稳定覆盖深状态机与并发交互。
• 调试成本高：越是复杂的 bug，越容易出现“仿真通过、芯片失败”。
• 需求可验证化：规格中的安全性、公平性、互斥性需要严格的数学判定。

1.2 核心概念

形式化验证是把设计视为数学模型，通过求解算法证明其所有可达行为是否满足一组属性。Cadence JasperGold 将 RTL、约束和 SystemVerilog Assertions（SVA）统一读入形式化求解环境。

• DUV（Design Under Verification）：待验证设计，通常是 RTL 模块或子系统。
• Property / Assertion：描述设计必须满足的行为属性，如互斥、公平性、超时响应。
• Constraint：限定输入环境，避免证明引擎探索无意义状态。
• Proof：证明属性在所有可达状态下都成立。
• Counterexample：违反属性的反例路径，可被 JasperGold 输出为波形。

图1-1 JasperGold 形式化求解链路

1.3 原理机制

JasperGold 的内部核心是“模型检查 + SAT/SMT 求解 + 反例生成”。它先将 RTL 转换为可操作的形式化模型，再把 SVA 属性转化为求解目标，最后穷举状态空间进行证明。

1. 建模：将时序逻辑、状态机与组合逻辑转换为可数学求解的结构。
2. 约束注入：把 assume/reset/环境约束加入模型，剪掉不可达状态。
3. 属性判定：对每个断言执行 bounded prove 或 unbounded/full prove。
4. 反例输出：若属性不成立，生成可回溯波形；若成立，返回 PASS。

1.4 实战流程步骤

一个标准 JasperGold 验证任务可以按下述流程组织：

1. 梳理设计边界与时钟复位，确认形式化验证目标。
2. 编写 SVA 断言，先写“安全属性”：互斥、无越界、状态不跳飞。
3. 补充约束：合法的输入范围、合理 stall、复位序列。
4. 读取设计、断言、约束文件进入 JasperGold。
5. 执行证明，优先收敛小的、重要的属性。
6. 分析结果：PASS 转向回归；FAIL 打开反例波形定位原因。

典型命令片段：

# 读入待验证设计
read_file -type sverilog ./rtl/arbiter.sv

# 读入断言与绑定文件
read_file -type sverilog ./tb/arbiter_bind.sv

# 设置时钟与复位
set_clock -name clk -period 10
set_reset -name rst_n -active low

# 执行形式化证明
prove -property arbiter_bind.port0_served

1.5 案例说明：仲裁器公平性验证

假设一个 4 端口仲裁器需要保证：当端口 0 发出请求后，不应被无限期占用。

property port0_served;
  @(posedge clk)
  req[0] |-> ##[1:2] grant[0];
endproperty

assert property (port0_served);

该属性要求：若 req[0] 拉高，则 grant[0] 必须在一个或两个周期内被拉高。若仲裁算法存在饿死风险，JasperGold 会返回 Falsified 并生成反例波形；若算法公平，则返回 PASS。

1.6 表格总结

概念	含义	在 JasperGold 中的落点
DUV	待验证设计	被读入并转换为形式化模型
Assertion / Property	期望的设计行为	通过 SVA 断言文件声明
Constraint	输入限制与环境假设	使用 assume / restrict 描述
Proof	对所有可达状态验证	JasperGold 引擎执行 full prove
Counterexample	破坏属性的输入序列	输出为波形，进入调试流程

1.7 误区提醒

1.8 实践清单