第二讲：SVA语法入门——序列、属性与断言指令

各位同学，今天我们来聊聊SVA最核心的三个概念：序列（sequence）、属性（property）和断言指令（assert/assume/cover）。

说实话，我刚接触SVA那会儿，也被这三个东西绕得晕头转向。后来做了几个项目才明白——它们其实就是一套层层递进的逻辑表达工具。你想想看，就像盖房子：序列是砖块，属性是墙体，断言指令就是质检员。

一、序列（sequence）——最基础的砖块

序列是什么？说白了就是描述信号在一段时间内的行为模式。比如“a信号拉高后，下一个时钟周期b信号也拉高”，这就是一个最简单的序列。

我个人习惯把序列理解成“事件的时序组合”。它关注的是信号在时钟边沿上的变化关系。

基本语法

sequence seq_name;
  signal1 ##n signal2;  // ##n 表示延迟n个时钟周期
endsequence

这里有个关键符号：##。它表示时钟周期的延迟。##1延迟一个周期，##0表示同一周期，##[1:3]表示延迟1到3个周期。

sequence req_ack;
  req ##1 ack;  // req拉高后，下一周期ack必须拉高
endsequence

我在项目中遇到过这样一个坑：有人写##1以为是一个时钟周期后，结果仿真发现是上升沿到下一个上升沿。嗯，这里要注意，##1确实是一个时钟周期，但如果你用时钟下降沿采样，那就要小心了。

序列的复合操作

序列可以组合使用，就像搭积木：

• and：两个序列都发生
• or：任一序列发生
• intersect：两个序列同时开始且同时结束
• within：一个序列在另一个序列的时间范围内发生

sequence seq_a_and_b;
  seq_a and seq_b;  // 两个序列都满足
endsequence

sequence seq_a_within_b;
  seq_a within seq_b;  // seq_a发生在seq_b的时间窗口内
endsequence

二、属性（property）——把砖块砌成墙

属性是在序列的基础上加了“条件”和“范围”。它描述的是“在什么条件下，什么序列应该成立”。

说白了，属性就是带逻辑判断的序列。它用|->（蕴含操作符）把条件和结果连起来。

两种蕴含操作符

property p_req_ack;
  @(posedge clk) req |=> ack;  // req拉高后，下一拍ack必须拉高
endproperty

属性还可以加disable iff来排除某些情况：

property p_req_ack_reset;
  @(posedge clk) disable iff (rst_n) req |=> ack;
endproperty

这个disable iff (rst_n)的意思是：复位期间不检查这个属性。我曾经见过有人忘了加这个，结果复位时一堆假失败，排查了半天才发现。

三、断言指令——质检员上场

序列和属性定义好了，谁来执行检查？就是这三个指令：assert、assume、cover。

assert（断言）

这是最常用的。它说：“我要求这个属性必须成立，如果不成立，就是设计错误。”

assert property (p_req_ack);  // 检查req_ack属性

仿真时如果违反，会打印错误信息。我在项目中一般会给每个assert加个名字和严重等级：

assert property (p_req_ack)
  else $error("req_ack协议违反！");

assume（假设）

这个有意思。它说：“我假设环境会满足这个条件，如果环境不满足，那就是测试平台的问题。”

assume主要用于形式化验证和约束随机仿真。它告诉工具：“别给我生成违反这个条件的激励。”

assume property (p_valid_ready);  // 假设valid和ready满足协议

cover（覆盖）

cover不检查对错，它只记录：“这个序列有没有发生过？”

为什么要用cover？你想想看，你写了一大堆断言，但有些场景可能仿真从来没跑到过。cover就是帮你确认：这些关键场景是否被覆盖到了。

cover property (p_req_ack);  // 记录req_ack发生的次数

我记得有一次做验证，功能覆盖率一直上不去。后来加了几个cover，才发现有个边界条件从来没触发过。嗯，这就是cover的价值。

四、知识体系总览

下面这张图帮你理清三者的关系：

五、实战中的避坑指南

最后分享几个我踩过的坑：

• 时钟域问题：序列和属性必须指定时钟。我见过有人忘了写@(posedge clk)，结果仿真跑得飞起，但断言一个都没触发。
• 重叠蕴含的陷阱：a |-> b要求a和b在同一周期成立。如果你想让b在下一周期成立，记得用|=> 。
• assume不是assert：assume是约束，不是检查。我曾经把assume当assert用，结果形式化验证工具报了一堆“矛盾约束”。
• cover要加名字：不加名字的cover，覆盖率报告里根本不知道哪个覆盖点被触发了。

好了，这一讲的内容就是这些。序列、属性、断言指令这三个概念，你只要记住“砖块-墙体-质检员”这个比喻，就不会搞混了。

可可精品资料库