systemverilog断言

### SystemVerilog 断言语法及使用示例

#### 什么是SystemVerilog断言？

SystemVerilog断言是一种用于硬件描述语言(HDL)中的验证机制，允许开发者定义预期行为并自动检查这些条件是否满足。这有助于早期发现错误，减少调试时间和成本。

#### 基础语法结构

断言通常由两部分组成：属性和动作。当指定的时间窗口内未满足给定的属性时，则执行相应的动作。以下是几种常见的断言语句：

- **立即断言 (Immediate Assertions)**: `assert` 关键字后面跟的是布尔表达式，在仿真过程中即时评估。

always @(posedge clk)
begin
    assert (reset_n === 1'b0 || state == IDLE);
end

- **并发断言 (Concurrent Assertions)**: 这些断言在整个模拟周期持续有效，并可以包含更复杂的序列逻辑[^1]。

#### 序列与属性

并发断言能够声明随时间发生的行为，并利用多层组合来创建复杂序列和属性。例如，下面的例子展示了一个简单的序列定义及其应用方式:

sequence seq_a;
    req ##1 gnt; // 请求之后的一个时钟周期获得授权
endsequence : seq_a

property prop_b;
    @(posedge clk) disable iff (!rst_n) seq_a |=> done;
endproperty : prop_b

这里定义了一种情况——即请求(req)发出后紧接着在一个时钟周期后的确认(gnt)，并且这种情况下最终会有一个完成(done)标志被置位。

#### 实际应用场景

为了帮助理解断言的具体用途，考虑如下场景：假设存在一个有限状态机(FSM), 需要确保其从初始态(start_state)经过一段时间(至少一次clk脉冲宽度)平稳过渡至下一个保持态(hold_next)[^4]:

// 定义状态转换路径作为序列
sequence start_to_hold_seq;
    start_state throughout $stable(state) [*1:$] ##1 hold_next;
endsequence : start_to_hold_seq

// 将上述序列应用于特定条件下触发的动作
assert property (@(posedge clk) start_to_hold_seq) else $error("FSM did not transition correctly");

这段代码片段说明了如何通过定义状态之间的关系来进行有效的验证测试。