17. 示例：用assert property检查FIFO空满标志冲突

前言

基于 SystemVerilog 的 FIFO 空满标志冲突检查（概念+实现+仿真全解）

一、概念解析与通俗理解

冲突定义
FIFO 的空标志（empty）和满标志（full）是互斥信号，任何时候都不应同时为高电平。若二者同时有效，说明 FIFO 的状态机或计数器存在逻辑错误，可能导致数据丢失或覆盖。

通俗理解
想象一个水杯（FIFO）：

• 当水杯空时（empty=1），不能倒出水（读操作无效）。
• 当水杯满时（full=1），不能倒入水（写操作无效）。
  若同时标记为“空”和“满”，说明杯子状态混乱，可能是计数器错误或读写指针同步问题。

概念：
assert property 是 SystemVerilog 中的一种断言机制，用于检查设计中的时序和逻辑关系。它可以用来验证信号之间的因果关系，确保设计符合预期的行为。

通俗理解：
assert property 就像一个“交通摄像头”，持续监控信号的时序关系。如果信号的变化不符合预期，它会立即发出警报，帮助你发现设计中的问题。

二、实现方式与代码示例

1. 核心断言逻辑

property fifo_empty_full_conflict;
  @(posedge clk) disable iff (rst) !(empty && full); // 每次时钟上升沿检查 empty 和 full 是否同时为高
endproperty

assert_fifo_conflict: assert property (fifo_empty_full_conflict)
  else $error("[FIFO ERROR] empty and full conflict at time %0t", $time);

通俗解释：

• 触发时机：每次时钟上升沿自动检查空满信号。
• 复位保护：复位期间（rst=1）跳过检查，避免误报。
• 错误处理：若断言失败，打印错误信息并记录时间戳。

2. 扩展场景（时序对齐）

若空满信号由组合逻辑生成（可能存在毛刺），需增加时序检查：

property fifo_conflict_stable;
  @(posedge clk) ##1 $stable(empty) && $stable(full) |-> !(empty && full);
endproperty

作用：检查空满信号稳定后是否冲突，避免因信号抖动误判。

3. 使用 assert property

实现方式：

1. 定义序列（sequence）：描述时序事件。
2. 定义属性（property）：封装序列和触发条件。
3. 使用 assert property：将属性绑定到设计中，进行检查。

通俗理解：
实现 assert property 就像编写一个规则，告诉仿真工具在什么情况下应该发生什么事情。如果事情没有按照规则发生，工具就会提醒你。

示例：

sequence s_ack_delay;
    req ##[1:3] ack;
endsequence

property p_ack_valid;
    @(posedge clk) req |-> s_ack_delay;
endproperty

ca_blk: assert property (p_ack_valid);

三、应用场景与示例

1. 验证阶段

• 仿真测试：在测试平台中绑定断言，捕捉边界条件（如读写指针同时回绕）。
• 形式验证：将断言作为形式验证目标，数学证明设计在所有场景下无冲突。

2. 实际案例

假设一个深度为 8 的同步 FIFO，若读写指针同时到达 0 且计数器溢出，断言会立即报错：

[FIFO ERROR] empty and full conflict at time 150ns

3. assert property 验证阶段

应用场景：

• 协议验证：检查 AXI 总线中的时序序列（如 addr 有效后 data 必须在指定周期内有效）。
• 状态机监控：确保状态转换符合预期（如状态 S1 必须跳转到 S2 而非 S3）。

通俗理解：
assert property 可以用来检查设计中的各种协议和状态机，确保它们的行为符合预期。比如，检查一个状态机是否按照设计的流程跳转，或者检查一个通信协议中的信号是否按照规定的时间顺序变化。

四、常见误区与规避方法

1. 忽略复位条件

错误写法：

property fifo_conflict_bad;
  @(posedge clk) !(empty && full); // 未处理复位
endproperty

问题：复位期间空满信号可能未初始化，导致误报。
修正：添加 disable iff (rst)。

2. 异步信号未同步

异步 FIFO 陷阱：
若空满信号跨时钟域未同步，直接断言会因亚稳态失败。
解决：

assert property (@(posedge wclk) !($sampled(empty) && $sampled(full)));

通过 $sampled() 确保信号稳定。

3. 时钟域的同步

常见误区：

• 忽略多时钟域同步问题：导致断言误报。
• 未正确指定采样时钟：导致断言检查的时序错误。

通俗理解：
在使用 assert property 时，需要注意时钟域的同步问题。如果设计中有多个时钟域，需要确保断言在正确的时钟域中采样信号。否则，可能会导致断言误报或者检查的时序错误。

示例：

property p_cross_clock;
    @(posedge clk1) $rose(sig1) |-> ##[1:2] @(posedge clk2) sig2;
endproperty

五、练习任务与讲解

任务1：设计 FIFO 空满保护断言

要求：当 FIFO 满时，写使能必须无效。
代码：

property fifo_full_block_write;
  @(posedge clk) disable iff (rst)
  full |-> !wr_en; // 满状态下禁止写操作
endproperty
assert_fifo_full: assert property (fifo_full_block_write);

讲解：

• full |-> !wr_en 表示若 full=1，则同一周期 wr_en 必须为 0。
• 若满状态下仍有写操作，断言会立即报错。

任务2： assert property 检查 FIFO 的空满标志冲突

练习任务：

1. FIFO 满标志检查：当 FIFO 满时，写使能必须无效。
2. 状态机合法跳转：确保状态机不能直接从 IDLE 跳转到 ERROR。
3. 立即断言验证握手协议：当 req 拉高时，ack 必须同一时刻拉高。
4. 并发断言验证数据稳定性：复位后，data 需在 2 个周期内保持稳定。
5. 设计 FIFO 的并发断言：检查 FIFO 满时 push 操作被阻塞。

通俗理解：
这些练习任务可以帮助你更好地理解和应用 assert property。通过编写和验证这些断言，你可以确保设计中的各种行为符合预期。

代码示例：

module fifo_assertions (
    input clk, rst_n,
    input wr_en, rd_en,
    input [7:0] wdata, rdata,
    input full, empty
);

// 立即断言：写满时禁止写入
always @(posedge clk) begin
    if (full) begin
        assert (!wr_en) else $error("满状态写入!");
    end
end

// 并发断言：连续写不越界
property p_write_flow;
    @(posedge clk) disable iff (!rst_n)
    wr_en && !full |=> !full until rd_en;
endproperty
assert property(p_write_flow);

endmodule

仿真步骤：

1. 编译与仿真命令：

xrun -64bit -access +rwc \
    -sv fifo_assertions.sv tb_fifo.sv \
    +define+ASSERT_ON \
    -covoverwrite \
    -nowarn UEXPSC

2. 查看结果：

• 断言失败时，日志会输出 $error 信息。
• 覆盖率报告（如 imc 工具）可显示断言触发情况。

预期输出：

Assertion failed: fifo_assertions.p_write_flow
  Time: 550ns  Scope: tb_fifo.fifo_assertions

这个示例展示了如何使用 assert property 检查 FIFO 的空满标志冲突，并通过 xrun 进行仿真验证。

六、完整仿真示例（Xrun 流程）

1. 文件结构

fifo.sv          # FIFO RTL 设计
fifo_assert.sv   # 断言模块
tb_fifo.sv       # 测试平台

2. 仿真命令

xrun -64bit -access +rwc \
  -sv fifo.sv fifo_assert.sv tb_fifo.sv \
  +define+ASSERT_ON \
  -covoverwrite \
  -nowarn UEXPSC

3. 测试平台示例

module tb_fifo;
  bit clk, rst;
  logic empty, full;

  // 时钟生成
  always #5 clk = ~clk;

  // 绑定 FIFO 设计
  fifo u_fifo (.*);

  initial begin
    rst = 1;
    #10 rst = 0;
    // 触发冲突场景：强制空满同时为高
    force u_fifo.empty = 1;
    force u_fifo.full = 1;
    @(posedge clk);
    release u_fifo.empty;
    release u_fifo.full;
    #20 $finish;
  end
endmodule

4. 预期输出

ncsim> run
[15ns] [FIFO ERROR] empty and full conflict at time 15ns
# Simulation complete

七、总结

• 断言价值：通过 assert property 可高效捕捉 FIFO 设计漏洞，减少调试时间。
• 跨域扩展：结合覆盖率（如 cover property）可验证边界场景，形式验证可深度分析时序逻辑。
• 避坑指南：关注复位、信号稳定性、跨时钟域同步等细节。