4. SystemVerilog断言基础：立即断言与并发断言、assert/assume/cover的用法

各位同学，今天我们来聊聊断言。说实话，我刚入行那会儿，觉得断言就是个“花架子”——代码写都写完了，还加这些检查干嘛？直到有一次，一个隐蔽的状态机跳转错误在仿真跑了三天才被发现，我花了整整一周去定位。从那以后，我再也不敢轻视断言了。

断言，说白了就是给设计加个“监控摄像头”。它不参与功能逻辑，但时刻盯着关键信号，一旦出问题立刻报警。在状态机验证中，断言能帮我们捕捉那些“不该发生却发生了”的异常跳转。

4.1 立即断言 vs 并发断言

SystemVerilog里断言分两种：立即断言和并发断言。它们名字听着像，但用法完全不同。

4.1.1 立即断言

立即断言，就是“现在立刻检查”。它写在过程块（always、initial）里，跟$display一样是顺序执行的。我习惯把它用在组合逻辑检查上。

// 立即断言示例
always_comb begin
    // 状态机状态不能为X或Z
    assert (state !== 2'bxx && state !== 2'bzz)
        else $error("状态机状态异常: %b", state);
end

注意看，这里用的是assert关键字，后面跟一个条件表达式。条件为真就通过，为假就执行else分支。我个人习惯在else里加上$error或$fatal，这样仿真一跑起来就能看到红色报错。

4.1.2 并发断言

并发断言，是“持续监控”的。它基于时钟沿采样，可以描述跨周期的时序关系。这才是状态机验证的主力。

// 并发断言示例
property p_state_transition;
    @(posedge clk)
    (state == IDLE) |=> (state == READ || state == WRITE);
endproperty

a_state_transition: assert property (p_state_transition);

这里|=>表示“下一个时钟沿”。意思是：如果当前状态是IDLE，那么下一个时钟沿状态必须是READ或WRITE。你想想看，这种跨周期的检查，立即断言根本做不到。

4.2 assert / assume / cover 三兄弟

这三个关键字，我管它们叫“断言三兄弟”。功能不同，但配合起来威力巨大。

4.2.1 assert —— 必须成立

assert是最常用的。它表示“这个条件必须永远成立”。如果仿真中assert失败，说明设计有bug。

// 状态机不能进入非法状态
assert property (
    @(posedge clk)
    disable iff (rst)
    !(state inside {ILLEGAL1, ILLEGAL2, ILLEGAL3})
);

disable iff (rst) 是复位时禁用检查，这个技巧我在项目里几乎每个断言都会用。不然复位期间一堆X态，断言会乱报。

4.2.2 assume —— 假设成立

assume是给环境用的。它告诉仿真器：“我假设输入信号满足这个条件”。如果输入不满足，仿真器会报错，但这不是设计的问题，是测试平台的问题。

// 假设输入信号不会出现非法组合
assume property (
    @(posedge clk)
    !(req & ack)  // req和ack不能同时为高
);

嗯，这里要注意：assume在形式验证里特别有用。它约束了输入空间，让工具只验证合法的输入序列。我在做形式验证时，assume写得比assert还多。

4.2.3 cover —— 覆盖检查

cover是“有没有发生过”。它不检查对错，只记录覆盖率。比如我想知道状态机有没有进入过某个状态序列：

// 覆盖：IDLE -> READ -> DONE 这个序列是否发生过
cover property (
    @(posedge clk)
    (state == IDLE) ##1 (state == READ) ##1 (state == DONE)
);

cover的结果会体现在覆盖率报告里。如果某个cover点从来没被触发过，说明你的测试用例没覆盖到那条路径。我一般会在每个状态转移路径上都加cover，这样跑完仿真一看报告，就知道哪些路径测过了，哪些还没测。

4.3 状态机验证中的实战技巧

说了这么多理论，来点实际的。下面是我在项目中总结的几个断言模板，直接拿去用。

4.3.1 状态唯一性检查

状态机在同一时刻只能处于一个状态。这个用one-hot编码时尤其重要。

// 状态唯一性：任何时候只有一个状态位为高
assert property (
    @(posedge clk)
    $onehot(state)
);

4.3.2 状态转移合法性检查

每个状态只能转移到允许的下一个状态。这个需要根据状态转移图来写。

// IDLE状态只能转移到READ或WRITE
assert property (
    @(posedge clk)
    (state == IDLE) |=> (state inside {READ, WRITE})
);

4.3.3 输出信号与状态关联检查

某些输出信号只在特定状态下有效。比如数据有效信号只在DONE状态为高。

// data_valid只在DONE状态为高
assert property (
    @(posedge clk)
    data_valid |-> (state == DONE)
);

4.4 本章知识体系

下面这张图总结了断言的核心逻辑，我画了很久，希望能帮你理清思路。

这张图从左到右展示了：断言分两类 → 各有特点 → 三兄弟各司其职 → 最终落到状态机验证。你写断言时，先想清楚用立即还是并发，再选assert/assume/cover，最后套用模板。

好了，这一章的内容就到这里。断言这东西，光看没用，得动手写。我建议你找个简单的状态机，试着给每个状态转移都加上assert和cover，跑一遍仿真看看效果。遇到问题随时来问我。