1. 课程导入

在数字芯片与FPGA设计流程中，功能仿真只能证明“某些激励下结果正确”，却无法回答两个更根本的问题：设计在所有合法输入下是否永远不会进入危险状态？修改后的RTL与原始RTL在功能上是否完全等价？前者属于安全属性验证（Safety Property Verification），后者属于逻辑等价验证（Logical Equivalence Checking，LEC）。Jasper是Cadence公司推出的形式验证平台，围绕这两类问题提供了一整套可工程化落地的工具链。本课程将围绕Jasper的实际使用展开，从属性描述、约束建模、证明策略，一直讲到等价检查与反例分析。

1.1 Jasper工具链概览

Jasper的核心是jg（JasperGold）命令环境，它把形式验证拆解为若干可独立调用的能力模块。理解这些模块的职责，是后续所有操作的基础。

• Property Specification：用SVA（SystemVerilog Assertion）或PSL描述待证属性，例如“请求发出后3个周期内必须收到应答”。
• Constraint Modeling：用assume、clock、reset等约束限定环境的合法行为，避免验证器探索物理上不可能出现的输入组合。
• Proof Engine：包括prove、bmc（有界模型检查）、k-induction等引擎，负责在状态空间中搜索反例或完成归纳证明。
• Coverage & Debug：通过cover属性检查场景可达性，通过反例波形（Counterexample Waveform）定位失败原因。
• Equivalence Checking：用lec或Jasper LEC流程比较两个设计在相同输入下的输出一致性，常用于RTL与网表、修改前后版本的比对。

这些模块并非孤立存在，而是共享同一套设计数据库、时钟复位定义和约束集合。一个典型的Jasper会话通常先读入设计，再定义时钟与复位，随后加载属性或等价检查脚本，最后调用证明引擎并分析结果。

1.2 安全属性验证的目标

安全属性验证要回答的是“坏事情永远不会发生”。在形式化语境中，“坏事情”被写成一条断言，验证器试图证明该断言在所有可达状态下恒为真。若证明失败，工具会给出从初始状态到违反断言的一条具体路径，即反例。

以一个小型仲裁器为例，其安全属性可以写成：

property no_double_grant;
  @(posedge clk) disable iff (!rst_n)
  !(grant[0] && grant[1]);
endproperty
assert property (no_double_grant);

这条属性表达的是：任意时钟上升沿，只要复位有效，两个授权信号不能同时为高。若Jasper返回proven，说明在所有合法输入序列下该条件都成立；若返回cex（反例），则需要检查是设计缺陷还是约束不足。

安全属性验证的难点通常不在写断言，而在约束的准确性。约束过松，验证器会探索非法输入并产生假反例；约束过紧，则可能掩盖真实缺陷。因此，assume与assert的边界划分是本节后续反复训练的核心技能。

1.3 逻辑等价验证的目标

逻辑等价验证要回答的是“两个设计是否在功能上完全一致”。它不关心内部结构，只关心在相同输入序列下，两个设计的输出是否始终相同。典型场景包括：RTL修改后与修改前比对、综合网表与RTL比对、不同优化策略下的网表比对。

Jasper LEC的基本做法是：把两个设计并排放入同一个验证环境，共享相同的输入激励，然后对每个输出端口建立assert比较点。若所有比较点都被证明恒等，则两个设计等价；若出现反例，则说明存在某个输入序列使输出不同。

与安全属性验证不同，等价验证通常不需要用户手写大量属性，而是由工具自动生成比较点。但用户仍需处理时钟定义、复位映射、黑盒（blackbox）匹配、常数寄存器等工程问题。例如，若两个设计的复位极性不同，直接比较会失败，必须先做映射或约束。

1.4 整体学习路径

本课程共30章，按“工具认知—属性建模—证明策略—等价检查—工程实战”的顺序推进。前几章建立Jasper环境与基本命令的认知；中间章节深入SVA属性、约束、覆盖与反例分析；随后进入LEC流程、网表比对与复杂场景处理；最后通过综合案例把安全属性验证与等价验证串联起来。

学习过程中建议始终围绕一个可运行的小设计（如仲裁器、FIFO、状态机）进行练习。每学一个概念，就在Jasper中实际执行一次prove或lec，观察返回结果与波形。形式验证的能力提升，很大程度上来自对反例的反复解读和对约束的反复修正。

1.5 从“能跑通”到“能收敛”

初学者常把形式验证等同于“写几条断言然后点运行”。实际工程中，真正的挑战在于收敛：证明要么在有限时间内返回确定结果，要么因状态空间爆炸而长时间无结论。Jasper提供了多种手段应对这一问题，包括抽象（abstraction）、切分（partitioning）、假设强化（assume tightening）以及引擎切换。

本课程不会停留在命令罗列层面，而是围绕真实设计对象展开。例如，在讲解约束时，会以一个带优先级的总线仲裁器为对象，给出具体的输入端口、优先级编码和合法请求序列；在讲解LEC时，会以“RTL修改前后”和“RTL与综合网表”两组比对为例，说明时钟映射、复位映射和黑盒处理的实际写法。

接下来的章节将从Jasper的启动方式与基本命令开始，逐步建立完整的形式验证工作流。请先确保你有一个可用的JasperGold环境，并准备好一个简单的Verilog设计作为练习对象。