UVM时序检查与缺陷定位实战 - 第2节

一、为什么我们需要断言？

做验证这么多年，我越来越觉得断言是个好东西。说白了，断言就是给设计加个「监控探头」——你希望某个信号在某个时刻必须为高，或者某个状态转换必须合法，那就写个断言盯着它。

我记得刚入行那会儿，有个同事调试一个复杂的握手协议，仿真跑了三天才发现一个时序违规。后来加了断言，五分钟就定位到了问题。嗯，从那以后，我再也不敢不做断言了。

二、SystemVerilog 断言（SVA）概述

SVA 是 SystemVerilog 的一部分，专门用来描述设计的行为期望。它有两种基本形式：立即断言和并发断言。我个人习惯把立即断言当成「过程块里的检查点」，并发断言则是「独立运行的时序监视器」。

2.1 立即断言

立即断言写在过程块（always、initial）里，像 if-else 一样立即求值。它的语法很简单：

// 立即断言示例
always @(posedge clk) begin
    if (valid) begin
        assert (data !== 'x) else $error("data 在 valid 有效时出现 X 态！");
    end
end

这里要注意：立即断言是阻塞性的，仿真器遇到它会立刻检查。如果失败，默认会打印一条消息并继续执行（除非你设置了 fatal）。

2.2 并发断言

并发断言才是 SVA 的精髓。它基于时钟沿采样，可以描述跨越多个时钟周期的行为。语法上以 property 或直接 assert property 开头：

// 并发断言示例：req 有效后 2~5 个周期内 ack 必须为高
property p_req_ack;
    @(posedge clk) req |-> ##[2:5] ack;
endproperty

a_req_ack: assert property(p_req_ack) else $error("req 后 ack 未在 2~5 周期内到达");

并发断言是非阻塞的，它会在每个时钟沿自动检查。你想想看，这比手动写一堆 if-else 要优雅多少倍？

三、断言序列与属性

序列（sequence）和属性（property）是 SVA 的两个核心概念。我经常把它们类比成「短语」和「句子」——序列是基本的时间关系描述，属性则把序列组合成完整的检查逻辑。

3.1 序列（sequence）

序列描述信号之间的时序关系。最简单的序列就是两个事件用 ## 连接：

// 序列示例：req 有效后，下一个周期 grant 必须有效
sequence s_req_grant;
    req ##1 grant;
endsequence

这里 ##1 表示延迟一个时钟周期。你也可以用 ##[min:max] 表示一个范围：

// 序列：req 有效后 1~3 个周期内 grant 有效
sequence s_req_grant_range;
    req ##[1:3] grant;
endsequence

3.2 属性（property）

属性在序列的基础上加入逻辑运算符和蕴含操作符。最常用的是蕴含操作符 |->（重叠蕴含）和 |=>（非重叠蕴含）：

// 属性：每当 req 有效，下一个周期 grant 必须有效
property p_req_grant;
    @(posedge clk) req |=> grant;
endproperty

// 属性：每当 req 有效，同一周期 grant 必须有效（重叠）
property p_req_grant_overlap;
    @(posedge clk) req |-> grant;
endproperty

我个人更喜欢用 |=> ，因为它明确表示「下一个周期」，不容易产生歧义。

四、$rose、$fell、$stable 的使用

这三个系统函数是边沿检测的利器。它们分别检测信号的上升沿、下降沿和保持稳定。我几乎在每个项目里都会用到它们。

4.1 $rose——检测上升沿

$rose(signal) 在信号从 0 变为 1 的时钟沿返回真。注意它比较的是前一个时钟沿的值和当前时钟沿的值：

// 检测 req 的上升沿
property p_req_rise;
    @(posedge clk) $rose(req) |=> grant;
endproperty

4.2 $fell——检测下降沿

和 $rose 相反，$fell 检测信号从 1 变为 0：

// 检测 grant 的下降沿
property p_grant_fall;
    @(posedge clk) $fell(grant) |=> req;
endproperty

4.3 $stable——检测保持稳定

$stable(signal) 在信号值没有变化时返回真。这个在检查「保持时间」或「状态不变」的场景下特别有用：

// 当 hold 有效时，data 必须保持稳定
property p_data_stable;
    @(posedge clk) hold |=> $stable(data);
endproperty

五、知识体系总览

为了让你更直观地理解本章的内容结构，我画了一张图：

六、实战避坑指南

最后分享几个我这些年积累的经验：

• 不要滥用 $rose 和 $fell：它们会生成额外的硬件逻辑（在形式验证中）。如果只是检查电平，直接用信号本身就好。
• 注意时钟域：跨时钟域的断言要特别小心。我建议用两级同步后再做断言，否则很容易出现误报。
• 断言密度要适中：我见过有人每个信号都加断言，结果仿真速度慢了 10 倍。我的经验是：关键协议、状态机、握手信号必须加，内部数据通路可以少加。
• 善用 $stable：检查「不该变化的时候变了」比检查「该变化的时候变了」更容易发现问题。比如地址锁存期间地址线必须稳定，用 $stable 一抓一个准。

好了，这一章的内容就到这里。断言是 UVM 验证的基石，掌握了这些基础，后面我们才能更好地做时序检查和缺陷定位。