📚 课程目录第2章形式验证基础与Jasper工具链

2. 形式验证基础与Jasper工具链

形式验证（Formal Verification）不依赖测试向量，而是把设计的行为约束、断言和属性转换成数学命题，由求解器穷尽搜索状态空间，证明“所有可能输入下属性恒成立”，或给出反例波形。它与仿真最本质的差别在于：仿真回答“我跑到的这些场景对不对”，形式验证回答“是否存在任何场景让它出错”。因此形式验证的结论只有三种：证明通过（Proven）、发现反例（CEX，Counterexample）、以及因状态空间过大或约束不足而无法收敛（Inconclusive/Undetermined）。理解这三种结果，是使用 Jasper 工具链的前提。

一、形式验证的基本原理

形式验证的核心是“属性 + 约束 + 求解”。属性（Property）用 SVA/PSL 描述设计必须满足的时序关系，例如“请求发出后 3 个周期内必须收到应答”；约束（Constraint）描述合法输入空间，例如“读写信号不会同时有效”；求解器在约束限定的输入空间内，对属性做归纳证明或 BMC（Bounded Model Checking）有界搜索。若属性在 k 步内被证明对所有可达状态成立，则通过；若找到一条从复位到违例的路径，则输出反例波形。

Jasper 的证明引擎主要分为三类：BMC 用于快速找反例，深度有限；归纳法（Induction） 用于证明属性在所有深度成立；抽象与切分（Abstraction/Slicing） 用于把大设计化简为与属性相关的小逻辑，降低求解复杂度。实际项目中通常先用 BMC 快速暴露浅层 bug，再用归纳法证明深层属性，最后用抽象处理大规模模块。

形式验证不是“替代仿真”，而是与仿真互补：仿真覆盖典型场景，形式验证覆盖边界与穷尽场景。两者共用同一套 SVA 断言时，验证效率最高。

二、Jasper 产品家族与工具链定位

Cadence Jasper 是业界主流的形式验证平台，其产品家族围绕“属性验证、连接性验证、覆盖率、安全验证”展开。理解各组件定位，有助于在项目中选对工具、配对环境。

从图中可以看到，Jasper 工具链分为三层：最上方是统一的证明引擎，中间是按验证目标选择的应用组件，下方是许可证、计算资源和工程脚本构成的运行环境。实际使用时，先确定验证目标（属性证明、等价性检查还是安全验证），再选择对应组件，最后配置许可证与计算资源。

三、许可证与运行环境配置

Jasper 采用 FlexLM 许可证管理。典型配置流程如下：

# 1. 设置许可证服务器地址（Linux 环境）
export LM_LICENSE_FILE=5280@lic-server.company.com
# 或使用 Cadence 专用变量
export CDS_LIC_FILE=5280@lic-server.company.com

# 2. 验证许可证可达性
lmutil lmstat -c 5280@lic-server.company.com -a | grep Jasper

# 3. 启动 JasperGold 并检查版本
jaspergold -version

# 4. 在 Tcl 控制台中确认许可证特性
# 输出示例（示意）：
# JasperGold 2024.03
# License feature: JasperGold_Formal  available: 4

许可证配置中最常见的两个问题是：端口不通（防火墙拦截 5280）和特性不足（并发用户数已满）。前者用 telnet lic-server 5280 验证，后者用 lmstat 查看占用情况。若公司使用多台许可证服务器，可用逗号分隔：5280@lic1,5280@lic2。

计算资源方面，Jasper 的证明过程对内存和 CPU 敏感。建议为每个证明任务预留至少 8 GB 内存和 4 个 CPU 核；对于大型 SoC 模块，32 GB 内存和 16 核更稳妥。临时目录应指向高速本地盘，避免 NFS 延迟导致求解变慢。工程脚本通常包含文件列表、时钟复位定义、约束文件和属性文件，例如：

# jasper_run.tcl 示例（示意）
analyze -sv09 -f filelist.f
elaborate -top top_module
clock clk -factor 1
reset -expression {!rst_n}
# 加载约束与属性
source constraints.sva
source properties.sva
# 设置证明策略
set_proofgrid_mode auto
set_engine_mode {BMC Induction}
# 运行证明
prove -all
# 查看结果
report -summary

四、从原理到工具链的衔接

理解原理后，工具链的使用就有了判断依据。例如，当 prove -all 返回 Inconclusive 时，不应盲目增加运行时间，而应先检查约束是否过松（导致状态空间爆炸）或属性是否过深（需要更强的归纳策略）。Jasper 提供的 set_proofgrid_mode、set_engine_mode 和抽象命令，正是把“原理”转化为“可操作策略”的接口。

形式验证的“证明通过”依赖于约束的正确性。如果约束写错（例如把非法输入空间排除掉），证明结果可能虚假通过。因此约束文件必须与设计规格严格对齐，并经过评审。

本节的核心是建立“原理—工具—环境”的完整认知：形式验证用数学方法穷尽状态空间，Jasper 用 BMC、归纳法和抽象把这一过程工程化，而许可证与计算资源是让工具链跑起来的基础条件。掌握这三层关系，后续的断言编写、约束建模和证明调试才有稳定的落脚点。