在 SystemVerilog Assertions (SVA) 中，sequence 和 property 是两个核心概念，它们既有区别又紧密相关。
1. 区别
| 特性 | sequence | property |
|---|---|---|
| 定义 | 描述一系列按时间顺序发生的事件模式 | 描述一个完整的断言条件，可以包含sequence |
| 时间性 | 关注时序上的事件序列 | 可以包含时序和非时序的断言 |
| 用途 | 作为构建property的基本模块 | 作为完整的断言语句 |
| 评估 | 不能直接用于断言，必须嵌入property中 | 可以直接用于assert、assume、cover语句 |
| 运算符 | 主要使用时序运算符(##, [*], [=]等) | 可使用逻辑运算符(and, or, not等)和蕴含操作符 |
2. 联系
-
层级关系：property 通常由 sequence 构建而成，sequence 是 property 的组成部分。
-
组合使用：多个 sequence 可以通过 property 组合成更复杂的断言。
-
蕴含操作：property 中常用 sequence 作为蕴含操作的前件(antecedent)。
3. 举例
3.1 sequence 示例
// 定义一个sequence：信号a为高后，在1个周期后b为高，再接着2个周期后信号c为高
sequence s1;a ##1 b ##2 c;
endsequence3.2 property 示例
// 定义一个property：如果reset为低，则上述sequence必须成立
property p1;@(posedge clk) !reset |-> s1;
endproperty// 使用property进行断言
assert property (p1);4. 总结
-
sequence 是描述时序模式的基本构建块，它本身不是完整的断言。
-
property 是完整的断言规范，可以包含时序和非时序条件，并能直接用于验证语句。
-
简单的断言可能只需要一个sequence，但复杂的断言需要将多个sequence组合成property。
-
property 可以包含蕴含操作(|->, |=>)和逻辑操作，而sequence主要关注事件的时序关系。
5. 举例
`timescale 1ns/10psmodule tb_top();logic clk, reset, req, ack;// 生成时钟（周期 10ns）initial beginclk = 0;forever #5 clk = ~clk;end// 生成复位信号initial beginreset = 1;#75 reset = 0; // 复位在 20ns 后释放end// 生成随机的 req 和 ack 信号（模拟设计行为）initial beginreq = 0;ack = 0;#30 req = 1 ; #20 req = 0 ;ack = 1;#25 req = 0 ;ack = 0;wait(reset == 0); // 等待复位结束repeat (10) begin@(posedge clk);req <= $random % 2; // 随机生成 reqif (req) begin@(posedge clk);ack <= 1; // 如果 req=1，则在下一周期 ack=1@(posedge clk);ack <= 0;endend#50 $finish; // 仿真结束end// 定义 sequence：检查 req 后 1~2 周期内 ack 为高sequence seq_req_ack;@(posedge clk) req ##[1:2] ack; // req 为高后，ack 在 1 或 2 周期后为高endsequenceinst1:assert property(seq_req_ack)$display("PASS: req/ack succeeded at time %0t", $time);else$error("ERROR: req/ack failed at time %0t", $time);// 定义 property：如果 req 为高，必须满足 seq_req_ackproperty p_handshake;@(posedge clk) disable iff (reset)req |-> seq_req_ack; // 蕴含操作符 |->endproperty// 断言检查inst2:assert property (p_handshake) $display("PASS: Handshake succeeded at time %0t", $time);else$error("ERROR: Handshake failed at time %0t", $time);// 覆盖点（可选）cover property (@(posedge clk) req ##[1:2] ack)$display("Covered req->ack at time %0t", $time);initial begin
$fsdbDumpfile("tb_top.fsdb");
$fsdbDumpvars(0,tb_top);
$fsdbDumpSVA(0,tb_top);
endendmodule
仿真结果如下：
