4. SVA属性(property)：属性定义、属性调用、属性与序列的关系

好，咱们今天聊聊SVA里最核心的概念——属性（property）。

说实话，我刚学SVA那会儿，总觉得序列（sequence）和属性（property）差不多，傻傻分不清。后来踩了几个坑才明白：序列是描述信号怎么变，属性是描述这个变化对不对。你想想看，序列就像你写的一段舞蹈动作，属性就是裁判来判断这段动作是否合规。

4.1 什么是属性？

属性，说白了就是一个带断言性质的表达式。它把序列组合起来，加上一些逻辑判断，最终输出一个true或false的结果。

我个人习惯把属性看作是“带裁判的序列”。序列只管描述事件的发生，属性则负责判断这个事件是否在正确的时机、以正确的方式发生。

4.2 属性的定义

属性的定义语法其实挺简洁的：

property property_name;
  // 逻辑表达式，可以包含序列、操作符、条件等
  @(posedge clk) disable iff (rst) sequence_expression;
endproperty

我来拆解一下：

• property_name：属性名字，随便起，但建议见名知意
• @(posedge clk)：时钟事件，所有时序都基于这个时钟
• disable iff (rst)：当rst为真时，禁用这个属性（不报错）
• sequence_expression：核心的序列表达式

我在项目中遇到过一种情况：有人把disable条件写成了disable iff (!rst)，结果复位时疯狂报错。嗯，这里要注意——disable iff后面跟的是“禁用条件”，不是“使能条件”。

4.3 属性的调用

定义好属性之后，怎么用呢？有两种方式：

4.3.1 直接断言

assert property (my_property);

这是最常用的方式。仿真时如果属性失败，会打印错误信息。

4.3.2 覆盖检查

cover property (my_property);

这个不报错，只统计属性被触发了多少次。我一般用它来检查某些关键路径是否被覆盖到。

4.3.3 假设约束

assume property (my_property);

这个用于形式验证，告诉工具“我假设这个条件永远成立”。

4.4 属性与序列的关系

这个关系，我用一张图来说明：

你看这张图就清楚了：序列是底层描述，属性是上层包装。一个属性可以包含多个序列，也可以包含逻辑操作符（如and、or、not）。

4.5 实战示例

来，咱们写一个完整的例子：

// 定义序列：请求后2个时钟周期内收到应答
sequence req_ack_seq;
  @(posedge clk) req ##2 ack;
endsequence

// 定义属性：在复位无效时，检查上述序列
property req_ack_property;
  @(posedge clk) disable iff (rst_n == 0)
    req |-> req_ack_seq;
endproperty

// 调用属性
assert property (req_ack_property);

这个例子很简单，但包含了所有核心要素：

• 序列：描述“req之后2拍出现ack”
• 属性：加上时钟、复位禁用、蕴含操作符|->
• 调用：用assert来检查

4.6 属性的组合操作

属性之间也可以组合，就像搭积木：

操作符	含义	示例
and	两个属性都成功	prop1 and prop2
or	至少一个成功	prop1 or prop2
not	属性失败才算成功	not prop1
if...else	条件判断	if (cond) prop1 else prop2

举个例子：

property combined_prop;
  @(posedge clk) disable iff (rst)
    (if (mode) 
       req_ack_property 
     else 
       no_req_property);
endproperty

这种写法在复杂设计中特别有用。我做过一个DMA控制器，根据不同的传输模式，断言检查的逻辑完全不同。用if...else一把搞定，比写多个属性清爽多了。

4.7 小结

好了，这一章的核心就这些：

• 属性是带裁判的序列，返回true/false
• 定义用property...endproperty，加上时钟和disable条件
• 调用有assert、cover、assume三种方式
• 序列是属性的基础，属性是序列的包装

下一章咱们会深入讲属性的各种操作符，特别是蕴含操作符|->和|=>的区别，那个才是真正容易搞混的地方。