📚 课程目录第2章属性描述语言入门

2. 属性描述语言入门

在 Jasper Formal 中，属性验证的核心输入是“属性（property）”，而属性通常由 SVA（SystemVerilog Assertions）或 PSL（Property Specification Language）描述。Jasper 本身并不要求你只使用某一种语言：它通过前端解析器把 SVA 与 PSL 统一映射到内部的属性语义模型，再交给形式引擎证明。理解这种映射关系，是写出可被工具正确理解、且能收敛的断言的第一步。

一、Jasper 如何“看懂”两种语言

Jasper 的验证流程可以概括为：设计 RTL 与属性文件一起读入，属性被解析为断言/覆盖/假设三类对象，随后进入形式引擎。SVA 与 PSL 在语法层差异明显，但在语义层共享同一套时序逻辑基础：布尔表达式、时序算子、时钟边沿、复位条件、蕴含关系。Jasper 的映射规则大致如下：

时钟与复位：SVA 用 @(posedge clk) 显式指定采样时钟，PSL 用 default clock 或 @(posedge clk) 声明默认时钟；Jasper 统一提取为属性的采样时钟域。
蕴含：SVA 的 |->（重叠蕴含）与 |=>（非重叠蕴含）对应 PSL 的 |-> 与 |=>，语义一致，仅书写符号不同。
时序算子：SVA 的 ##n 延迟、[*n] 重复、throughout、within 等，在 PSL 中分别对应 next[n]、[*n]、before/until 等结构，Jasper 在内部统一为时序窗口与序列匹配。
属性与序列：SVA 的 sequence...endsequence 与 property...endproperty，PSL 的 sequence 与 property 声明，Jasper 都映射为可复用的命名属性节点。

因此，选择 SVA 还是 PSL，更多取决于团队习惯与设计语言生态，而不是工具能力。对 SystemVerilog 设计，SVA 更自然；对 VHDL 或混合语言项目，PSL 往往更统一。

二、基本断言编写：从“信号关系”到“时序窗口”

写断言时，先明确要验证的“设计意图”，再把它翻译成时序表达式。以常见的请求-应答握手为例，设计意图是：当 req 拉高后，ack 必须在 1 到 3 个时钟周期内拉高。用 SVA 可以写成：

property p_req_ack;
  @(posedge clk) disable iff (!rst_n)
  req |-> ##[1:3] ack;
endproperty
assert property (p_req_ack);

对应的 PSL 写法为：

property p_req_ack is
  always ({rst_n; req} |-> next[1 to 3] ack);
end property;
assert p_req_ack;

两者在 Jasper 中会被解析为同一条“req 有效后，ack 在 1~3 周期内有效”的时序属性。注意 disable iff (!rst_n) 与 PSL 中 rst_n 作为前提条件的写法，都是为了让复位期间不产生误报。

三、SVA 与 PSL 的映射对照

下表列出 Jasper 中最常用的语法映射，便于在两种语言间切换：

语义	SVA 写法	PSL 写法
采样时钟	`@(posedge clk)`	`default clock = (posedge clk);`
重叠蕴含	`a \|-> b`	`a \|-> b`
非重叠蕴含	`a \|=> b`	`a \|=> b`
延迟 n 周期	`##n`	`next[n]`
延迟区间	`##[1:3]`	`next[1 to 3]`
重复	`[*n]`	`[*n]`
复位禁用	`disable iff (!rst_n)`	`rst_n -> ...` 或 `abort`

需要强调的是，映射不是“逐字符替换”，而是语义等价。例如 SVA 的 disable iff 是异步复位语义，PSL 中常用 abort 或前提条件表达，Jasper 会根据上下文选择正确的复位处理方式。写断言时应优先保证语义正确，再考虑语法风格。

四、编写可收敛断言的三条实践原则

第一，时钟域要单一。一条属性只使用一个采样时钟，跨时钟域检查应拆成多条属性或使用同步器模型，否则形式引擎难以收敛。第二，时序窗口要有限。像 ##[1:$] 这种无界延迟会让证明空间爆炸，应尽量写成 ##[1:3] 这类有界区间。第三，假设与断言分离。用 assume 约束输入环境，用 assert 描述待证性质，Jasper 才能正确划分“前提”与“结论”。

在 Jasper 中，SVA 与 PSL 可以混用，但同一属性文件内建议保持风格一致，便于维护和复用。若设计是 SystemVerilog，优先用 SVA；若设计是 VHDL 或混合语言，PSL 的 default clock 机制更统一。

五、从断言到证明：Jasper 中的属性生命周期

一条属性进入 Jasper 后，会经历“解析 → 绑定 → 假设提取 → 证明”四个阶段。解析阶段把 SVA/PSL 转成内部时序表达式；绑定阶段把属性中的信号连接到设计网表；假设提取阶段把 assume 和 disable iff 转为约束；证明阶段由形式引擎判定属性是否在所有合法输入下成立。若属性被证伪，Jasper 会给出反例波形，反例中的信号变化正是调试断言的直接依据。

图中展示了 SVA 与 PSL 两条输入路径如何汇入 Jasper 前端解析器，再经过绑定、假设提取、形式证明，最终得到“证明”或“反例”两种结果。反例波形会反馈回断言调试环节，形成闭环。理解这条链路，有助于在写断言时预判工具的行为：哪些写法会让证明空间变大，哪些约束能帮助收敛，哪些反例是设计缺陷而非断言错误。

最后给出一个可直接参考的断言模板，用于验证“状态机不会进入非法状态”：

// SVA 版本
property p_no_illegal_state;
  @(posedge clk) disable iff (!rst_n)
  !(state == ILLEGAL);
endproperty
assert property (p_no_illegal_state);

// PSL 版本
property p_no_illegal_state is
  always ({rst_n; state /= ILLEGAL});
end property;
assert p_no_illegal_state;

在 Jasper 中运行后，若返回“proven”，说明在所有合法输入与复位条件下，状态机都不会进入 ILLEGAL；若返回“cex”，则反例波形会显示进入 ILLEGAL 的具体路径，此时应检查是状态编码遗漏、复位不完整，还是断言本身缺少必要的假设约束。掌握这种“写属性—跑证明—读反例—修断言或设计”的循环，就真正进入了形式验证的实践节奏。