4、断言与时序检查：SVA基础语法、assert property的使用、cover property的覆盖率收集

4.1 为什么我们需要断言？

做验证这么多年，我越来越觉得断言是个好东西。说白了，断言就是给设计加个“监控摄像头”。你想想看，我们写testbench跑仿真，通常只会在最后检查输出对不对。但中间那些关键信号的变化呢？有没有违规？有没有出现不该有的毛刺？

我在项目中遇到过好几次这样的情况：仿真跑完了，功能也对，但后仿就是过不了。查到最后，发现是某个握手信号时序出了问题。要是早点加上断言，这种问题在RTL阶段就能抓出来。

断言的核心价值就两点：

• 实时监控：信号变化的那一刻就能发现问题，不用等到最后比对
• 精确定位：断言失败会告诉你具体在哪个时间点、哪个信号出了问题

4.2 SVA基础语法——入门其实不难

SVA（SystemVerilog Assertions）的语法，说白了就两种：并行的和时序的。咱们先从最基础的开始。

4.2.1 立即断言 vs 并发断言

类型	关键字	特点	使用场景
立即断言	assert (expr)	组合逻辑，立即检查	简单的组合条件检查
并发断言	assert property	时序逻辑，基于时钟	复杂的时序关系检查

嗯，这里要注意：并发断言才是UVM验证中的主力。立即断言太简单，一般只在initial块里用用。

4.2.2 序列（sequence）——断言的基本单元

序列是什么？就是一组信号在时间上的排列。我习惯把它理解成“信号的舞蹈动作”。

// 最简单的序列：信号a在时钟上升沿为高
sequence s_a_high;
  @(posedge clk) a;
endsequence

// 带延迟的序列：a为高后，过两个时钟周期b为高
sequence s_a_then_b;
  @(posedge clk) a ##2 b;
endsequence

// 重叠序列：a为高时，b也为高
sequence s_a_and_b;
  @(posedge clk) a && b;
endsequence

这里面的##2表示延迟两个时钟周期。我曾经犯过一个低级错误——把##2写成了##1，结果仿真怎么跑都不对。后来查了半天才发现是延迟周期数搞错了。这种坑，踩过一次就记住了。

4.2.3 属性（property）——序列的“包装盒”

序列只是描述了信号的变化，但真正用来做检查的是property。你可以把property理解成给序列加了个“包装盒”，里面可以放触发条件、使能信号等。

// 基本属性：当reset为低时，检查a为高后两个周期b为高
property p_req_ack;
  @(posedge clk) disable iff (reset)
    a |=> ##2 b;
endproperty

// 另一种写法：使用蕴含操作符
property p_req_ack_v2;
  @(posedge clk) disable iff (reset)
    a |-> ##2 b;
endproperty

这里有两个操作符要注意：

• |->：重叠蕴含。左边条件满足时，同一个时钟周期检查右边
• |=>：非重叠蕴含。左边条件满足时，下一个时钟周期开始检查右边

4.3 assert property——让断言真正工作起来

有了property，怎么让它跑起来？用assert property。这是SVA中最核心的语句。

// 在module中直接使用
assert property (p_req_ack)
  else $error("req-ack协议违例！");

// 在interface中使用
interface ahb_if (input clk, reset);
  // ... 信号声明 ...
  
  property p_hwrite_setup;
    @(posedge clk) disable iff (reset)
      hsel |=> $stable(hwrite);
  endproperty
  
  assert property (p_hwrite_setup)
    else $fatal("hwrite在hsel有效期间不能变化");
endinterface

assert property的完整语法是这样的：

assert property (property_name) [action_block]

action_block可以写：

• $info：信息提示，不中断仿真
• $warning：警告，不中断仿真
• $error：错误，默认不中断，但工具会统计
• $fatal：致命错误，立即中断仿真

4.4 cover property——别让断言白写了

断言不仅能抓bug，还能做覆盖率收集。这就是cover property的用处。

你想想看，你写了一个断言检查“请求后两个周期必须有应答”。如果仿真跑完了，这个断言从来没触发过，那说明什么？要么是设计没走到这个场景，要么是你的testbench没覆盖到。这两种情况都需要关注。

// 收集覆盖率：检查req_ack序列是否被触发过
cover property (p_req_ack)
  $display("req_ack序列被触发了");

// 更精细的覆盖率：检查特定值的组合
cover property (@(posedge clk) (addr == 32'hA000_0000) ##1 (data == 32'hDEAD_BEEF));

cover property的语法和assert property几乎一样，只是关键字从assert换成了cover。但它们的用途完全不同：

功能	assert property	cover property
目的	检查正确性	收集覆盖率
失败时	报错/中断	不报错
成功时	不记录	记录一次命中
典型用法	检查协议违例	检查边界场景是否被覆盖

4.5 实战：一个完整的AHB握手断言

说了这么多，咱们来写个完整的例子。假设我们要检查AHB总线的hready握手协议：

// 定义序列
sequence s_hready_handshake;
  @(posedge hclk)
    hsel && hready_in ##1 hready_out;
endsequence

// 定义属性
property p_hready_handshake;
  @(posedge hclk) disable iff (hresetn)
    hsel && hready_in |=> hready_out;
endproperty

// 断言检查
assert property (p_hready_handshake)
  else $error("hready握手失败：hsel有效后下一周期hready_out必须为高");

// 覆盖率收集
cover property (s_hready_handshake)
  $display("hready握手序列被触发");

这个例子虽然简单，但包含了SVA的核心要素：序列定义、属性封装、断言检查、覆盖率收集。你在实际项目中，可以把这种模式套用到各种协议检查上。

4.6 知识体系总览

下面这张图是我自己整理的SVA知识体系，你可以把它当成一个“地图”，随时回来对照：

4.7 避坑指南

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

• 时钟域问题：我曾经把两个不同时钟域的信号放在同一个断言里，结果仿真结果完全不可预测。记住：一个断言只能在一个时钟域下工作。跨时钟域要用专门的同步器处理。
• disable iff的位置：disable iff要写在property的最前面，写在后面可能不生效。这个坑我踩了两次才记住。
• 仿真性能：断言写太多确实会影响仿真速度。我的做法是：功能验证阶段全开，回归测试时只开关键断言。
• 不要过度依赖$fatal：$fatal会直接杀掉仿真，导致你拿不到后面的波形。除非是致命错误，否则用$error就够了。

可可精品资料库