📚 课程目录第4章属性描述语言SVA与PSL

4. 属性描述语言SVA与PSL

在Jasper形式验证体系中，属性描述语言是连接设计意图与验证引擎的桥梁。SVA（SystemVerilog Assertions）与PSL（Property Specification Language）是两种最常用的属性描述语言，它们都基于时序逻辑，能够精确表达“在什么条件下、经过多长时间、信号之间应满足什么关系”。本节将围绕这两种语言的语法结构、序列与属性的构建方式，以及断言、假设、覆盖指令的编写方法展开，帮助读者建立从自然语言需求到可执行属性的完整转化能力。

一、SVA与PSL的定位与选择

SVA是SystemVerilog标准的一部分，天然嵌入在SystemVerilog代码中，适合与RTL设计紧密耦合的验证场景。PSL则是一种独立的属性描述语言，可以通过绑定文件与Verilog/VHDL设计关联，在多语言混合项目中更具灵活性。在Jasper中，两者都可以被解析并转化为内部的形式化模型。选择哪一种，通常取决于设计源码的语言、团队既有习惯以及是否需要跨语言复用属性。

从语法风格看，SVA使用assert property、assume property、cover property等关键字，序列和属性通过sequence...endsequence、property...endproperty定义。PSL则使用assert、assume、cover指令，并常以--或//注释风格书写，属性通过property...endproperty定义。两者在时序算子上的表达力相近，但书写习惯不同。

二、序列：描述信号随时间的变化

序列是SVA/PSL中最基础的时序描述单元，它回答的是“信号在时间轴上如何变化”。SVA中序列用sequence...endsequence定义，PSL中则直接写在属性表达式里。核心时序算子包括：

##n：延迟n个时钟周期。例如a ##2 b表示a成立后，经过2个时钟周期b成立。
##[m:n]：延迟m到n个周期中的任意一个。例如req ##[1:3] ack表示req之后1到3个周期内ack出现。
[*n]：连续重复n次。例如valid[*4]表示valid连续4个周期为高。
[*m:n]：连续重复m到n次。
|->和|=>：蕴含算子。前者表示同一周期内前提成立则结论成立，后者表示下一周期结论成立。

举例来说，一个典型的握手协议可以描述为：当req拉高后，在1到3个周期内ack必须拉高。SVA写法为：

sequence handshake_seq;
  req ##[1:3] ack;
endsequence

PSL中对应的写法为：

sequence handshake_seq is
  {req; [*1 to 3]; ack};
endsequence

注意PSL使用分号表示时序连接，[*1 to 3]表示延迟1到3个周期。两者语义一致，但书写风格不同。

三、属性：序列与触发条件的组合

属性在序列的基础上增加了“何时检查”的语义。一个属性通常由触发条件和序列组成，常见形式为always (条件 |-> 序列)或always (条件 |=> 序列)。SVA中属性用property...endproperty定义，PSL中同样使用property...endproperty。

继续上面的握手例子，我们要求“只要req拉高，就必须在1到3个周期内看到ack”，SVA写法为：

property handshake_prop;
  @(posedge clk) disable iff (rst_n == 0)
  req |-> ##[1:3] ack;
endproperty

其中@(posedge clk)指定采样时钟，disable iff (rst_n == 0)表示复位期间不检查。PSL写法为：

property handshake_prop is
  always ({rst_n; req} |-> {[1 to 3]; ack});
endproperty

这里always表示在每个时钟周期都检查该属性，|->是蕴含算子。PSL中{rst_n; req}表示rst_n和req在同一周期成立。

四、断言、假设与覆盖指令

定义好属性后，需要通过指令将其绑定到验证环境中。三类核心指令各有明确用途：

指令	SVA写法	PSL写法	作用
断言	`assert property (p);`	`assert p;`	检查设计是否始终满足属性，违反则报错
假设	`assume property (p);`	`assume p;`	约束输入环境，排除非法激励
覆盖	`cover property (p);`	`cover p;`	检查场景是否可达，评估验证完备性

在Jasper中，断言用于证明设计正确性，假设用于缩小状态空间，覆盖用于确认激励能够触发目标场景。三者配合使用，才能形成完整的验证闭环。

实践提示：在编写假设时，要避免过度约束导致设计行为被掩盖。一个常见的做法是先用覆盖指令确认假设场景确实可达，再将其作为假设加入验证环境。

五、编写示例：从需求到可执行属性

假设有一个简单的FIFO设计，需求为：“当FIFO非空时，读使能有效后下一个周期读数据有效”。我们可以按以下步骤编写属性：

定义序列：!empty ##1 rd_en ##1 rd_valid
定义属性：always (!empty && rd_en |=> rd_valid)
绑定断言：assert property (fifo_read_prop);
添加覆盖：cover property (!empty && rd_en);

SVA完整写法：

property fifo_read_prop;
  @(posedge clk) disable iff (!rst_n)
  (!empty && rd_en) |=> rd_valid;
endproperty

assert property (fifo_read_prop);
cover property (!empty && rd_en);

PSL完整写法：

property fifo_read_prop is
  always ({!empty; rd_en} |=> {rd_valid});
endproperty

assert fifo_read_prop;
cover {!empty; rd_en};

在Jasper中加载这些属性后，工具会尝试证明断言是否成立。如果断言失败，会给出反例波形，显示在哪个周期、哪些信号导致了违反。如果覆盖失败，说明该场景在约束下不可达，需要检查假设是否过强或激励是否不足。

注意：SVA和PSL在时序算子的优先级和结合性上存在细微差异。例如SVA中##的优先级高于|->，而PSL中;的优先级需要结合具体语法确认。在跨语言复用属性时，建议先在小规模测试用例上验证语义一致性。

六、常见错误与排查

初学者在编写SVA/PSL时容易遇到以下问题：

时钟域混淆：属性中指定的时钟必须与设计实际时钟一致，否则采样点错误。
复位处理不当：未使用disable iff或等效机制，导致复位期间误报。
蕴含方向写反：|->和|=>的区别在于结论是在同一周期还是下一周期成立，写反会导致时序偏移一个周期。
假设过强：假设条件覆盖了所有可能输入，导致断言无法被触发，覆盖率为零。
序列重复次数错误：[*n]表示连续n次，而##n表示延迟n个周期，两者语义不同。

排查时，可以先用cover property确认序列是否可达，再用assert property检查属性是否成立。Jasper的反例波形和覆盖报告是定位问题的关键依据。

掌握SVA与PSL的语法、序列与属性构建方法，以及断言、假设、覆盖三类指令的编写技巧，是构建形式验证体系的基础。在实际项目中，建议从关键控制路径和协议接口入手，逐步积累属性库，并通过覆盖分析持续评估验证完备性。