3. 断言基础：SystemVerilog断言(SVA)概述、立即断言与并发断言、断言层次结构

3.1 什么是断言？为什么我们需要它？

各位好，咱们今天聊聊断言。说白了，断言就是给设计加个“监控摄像头”。你想想看，一个芯片几千万门，靠人眼去波形里找bug？那得找到猴年马月去。

我刚开始做验证那会儿，有个项目流片回来，发现某个状态机在特定条件下跑飞了。查了整整两周，最后发现是握手信号早了一个周期。要是当时有断言，这个问题在仿真第一天就能抓到。从那以后，我养成了一个习惯：没有断言，绝不开始仿真。

SystemVerilog断言（SVA）是SV语言里专门用来描述时序行为的“小语言”。它不参与设计逻辑，只负责监视。一旦发现违反规则，立刻报错。嗯，就是这么个角色。

3.2 立即断言 vs 并发断言

SVA分两大类：立即断言和并发断言。很多新手搞不清区别，我当年也迷糊过。咱们一个一个说。

3.2.1 立即断言

立即断言，顾名思义，执行到这一行就立刻检查。它像C语言里的assert()，是过程性语句，必须放在initial或always块里。

// 立即断言示例
always_comb begin
    a_ready_valid: assert (ready && valid) else
        $error("ready和valid不能同时为高");
end

注意看，这个断言在组合逻辑里，每个时钟周期都会执行。但它不关心时序，只检查当前时刻的值。我个人习惯在以下场景用立即断言：

• 检查组合逻辑的不变量（比如one-hot编码）
• 检查接口的静态约束（比如总线宽度）
• 在函数或任务里做参数合法性检查

3.2.2 并发断言

并发断言才是SVA的精髓。它基于时钟周期，可以描述跨多个周期的时序关系。说白了，它能检查“信号A拉高后，三个周期内信号B必须拉高”这种复杂场景。

// 并发断言示例
property p_req_ack;
    @(posedge clk) req |=> ##[1:3] ack;
endproperty

a_req_ack: assert property(p_req_ack)
    else $error("req后1-3周期内ack未拉高");

这里有个关键区别：并发断言是声明式的，它不写在过程块里，而是写在module或interface里。仿真器会在每个时钟沿自动采样并评估。

我记得有个项目，验证工程师写了200多条并发断言，覆盖了所有总线协议。结果仿真跑了三天，断言抓到了7个bug，其中3个是设计工程师自己都没意识到的边界情况。这就是断言的价值。

特性	立即断言	并发断言
执行方式	过程性，立即执行	声明式，时钟沿触发
时序能力	仅当前时刻	跨周期时序
放置位置	always/initial块内	module/interface/checker内
典型用途	组合逻辑检查	协议时序检查

3.3 断言层次结构

断言不是乱写的，它有一套清晰的层次结构。我习惯把它分成四层，从底向上分别是：

1. 布尔表达式：最基础的信号关系，比如 a && b
2. 序列（sequence）：多个布尔表达式按时间顺序组合，比如 a ##2 b
3. 属性（property）：在序列基础上加入时钟、使能、蕴含等逻辑
4. 断言声明：把属性实例化，并指定通过/失败时的行为

咱们用一张图来理解这个层次：

你看，从底层到顶层，表达能力越来越强。实际项目中，我通常这样组织：

• sequence：定义通用的时序模式，比如“请求后必须响应”
• property：在sequence基础上加时钟和使能条件
• assert/assume/cover：决定这个property是检查、假设还是覆盖率统计

3.4 三种断言声明：assert、assume、cover

SVA提供了三种声明方式，用途完全不同：

关键字	用途	失败时行为
assert	检查设计行为是否正确	报错（可配置严重级别）
assume	约束测试平台的激励	约束求解器使用，仿真中报错
cover	统计某个时序是否被覆盖到	不报错，只记录

我个人习惯这样分配：

• assert：检查设计本身，比如“FIFO满时不能写”
• assume：约束外部输入，比如“输入数据必须稳定在时钟沿前后”
• cover：验证场景是否被覆盖，比如“是否出现过背靠背传输”

举个例子，假设我们有个AHB总线接口：

// 断言：hwrite在hready高时不能变化
property p_write_stable;
    @(posedge hclk) disable iff(!hresetn)
    hready |=> $stable(hwrite);
endproperty
a_write_stable: assert property(p_write_stable);

// 假设：master不能同时发多个请求
property p_no_overlap;
    @(posedge hclk) disable iff(!hresetn)
    hreq |=> !hreq ##1 hreq;
endproperty
as_no_overlap: assume property(p_no_overlap);

// 覆盖：是否出现过burst传输
property p_burst;
    @(posedge hclk) hburst != 3'b000;
endproperty
c_burst: cover property(p_burst);

嗯，这里要注意：assume在仿真中也会报错，它只是告诉形式化验证工具“这是输入约束”。如果你在仿真里用assume，一旦违反，仿真器照样会报。所以assume更适合用在接口上，约束testbench的行为。

3.5 本章小结

断言是验证工程师的“第三只眼”。它不睡觉、不偷懒、不放过任何一个违规。咱们今天讲了：

• 立即断言和并发断言的区别——一个看当下，一个看时序
• 断言的四层结构——从布尔表达式到完整的断言声明
• 三种声明方式——assert检查、assume约束、cover统计

下一章咱们会深入SVA的序列语法，包括各种操作符和匹配技巧。到时候我会分享一些实际项目中踩过的坑，保证让你少走弯路。