IT评测·应用市场-qidao123.com

标题: 17. 示例：用assert property检查FIFO空满标志冲突 [打印本页]

---

作者: 泉缘泉    时间: 2025-3-9 03:47
标题: 17. 示例：用assert property检查FIFO空满标志冲突

---

前言

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

---

一、概念解析与通俗理解

冲突定义
FIFO 的空标志（empty）和满标志（full）是互斥信号，任何时间都不应同时为高电平。若二者同时有效，阐明 FIFO 的状态机或计数器存在逻辑错误，大概导致数据丢失或覆盖。
通俗理解
想象一个水杯（FIFO）：

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

概念：
assert property 是 SystemVerilog 中的一种断言机制，用于检查计划中的时序和逻辑关系。它可以用来验证信号之间的因果关系，确保计划符合预期的活动。
通俗理解：
assert property 就像一个“交通摄像头”，持续监控信号的时序关系。如果信号的变革不符合预期，它会立刻发出警报，资助你发现计划中的题目。

---

二、实现方式与代码示例

1. 核心断言逻辑

1. property fifo_empty_full_conflict;
2.   @(posedge clk) disable iff (rst) !(empty && full); // 每次时钟上升沿检查 empty 和 full 是否同时为高
3. endproperty
5. assert_fifo_conflict: assert property (fifo_empty_full_conflict)
6.   else $error("[FIFO ERROR] empty and full conflict at time %0t", $time);

复制代码

通俗表明：

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

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

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

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

复制代码

作用：检查空满信号稳固后是否冲突，制止因信号抖动误判。
3. 使用 assert property

实现方式：

• 定义序列（sequence）：描述时序变乱。
  
• 定义属性（property）：封装序列和触发条件。
  
• 使用 assert property：将属性绑定到计划中，进行检查。
  

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

1. sequence s_ack_delay;
2.     req ##[1:3] ack;
3. endsequence
5. property p_ack_valid;
6.     @(posedge clk) req |-> s_ack_delay;
7. endproperty
9. ca_blk: assert property (p_ack_valid);

复制代码

---

三、应用场景与示例

1. 验证阶段

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

2. 实际案例

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

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

复制代码

3. assert property 验证阶段

应用场景：

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

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

---

四、常见误区与规避方法

1. 忽略复位条件

错误写法：

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

复制代码

题目：复位期间空满信号大概未初始化，导致误报。
修正：添加 disable iff (rst)。
2. 异步信号未同步

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

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

复制代码

通过 $sampled() 确保信号稳固。
3. 时钟域的同步

常见误区：

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

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

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

复制代码

---

五、练习任务与解说

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

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

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

复制代码

解说：

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

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

练习任务：

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

通俗理解：
这些练习任务可以资助你更好地理解和应用 assert property。通过编写和验证这些断言，你可以确保计划中的各种活动符合预期。
代码示例：

1. module fifo_assertions (
2.     input clk, rst_n,
3.     input wr_en, rd_en,
4.     input [7:0] wdata, rdata,
5.     input full, empty
6. );
8. // 立即断言：写满时禁止写入
9. always @(posedge clk) begin
10.     if (full) begin
11.         assert (!wr_en) else $error("满状态写入!");
12.     end
13. end
15. // 并发断言：连续写不越界
16. property p_write_flow;
17.     @(posedge clk) disable iff (!rst_n)
18.     wr_en && !full |=> !full until rd_en;
19. endproperty
20. assert property(p_write_flow);
22. endmodule

复制代码

仿真步骤：

• 编译与仿真下令：
  

1. xrun -64bit -access +rwc \
2.     -sv fifo_assertions.sv tb_fifo.sv \
3.     +define+ASSERT_ON \
4.     -covoverwrite \
5.     -nowarn UEXPSC

复制代码

• 检察效果：
  

• 断言失败时，日记会输出 $error 信息。
  
• 覆盖率陈诉（如 imc 工具）可体现断言触发情况。
  

预期输出：

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

复制代码

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

---

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

1. 文件结构

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

复制代码

2. 仿真下令

1. xrun -64bit -access +rwc \
2.   -sv fifo.sv fifo_assert.sv tb_fifo.sv \
3.   +define+ASSERT_ON \
4.   -covoverwrite \
5.   -nowarn UEXPSC

复制代码

3. 测试平台示例

1. module tb_fifo;
2.   bit clk, rst;
3.   logic empty, full;
5.   // 时钟生成
6.   always #5 clk = ~clk;
8.   // 绑定 FIFO 设计
9.   fifo u_fifo (.*);
11.   initial begin
12.     rst = 1;
13.     #10 rst = 0;
14.     // 触发冲突场景：强制空满同时为高
15.     force u_fifo.empty = 1;
16.     force u_fifo.full = 1;
17.     @(posedge clk);
18.     release u_fifo.empty;
19.     release u_fifo.full;
20.     #20 $finish;
21.   end
22. endmodule

复制代码

4. 预期输出

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

复制代码

---

七、总结

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

免责声明：如果侵犯了您的权益，请联系站长，我们会及时删除侵权内容，谢谢合作！更多信息从访问主页：qidao123.com:ToB企服之家，中国第一个企服评测及商务社交产业平台。

---

欢迎光临 IT评测·应用市场-qidao123.com (https://dis.qidao123.com/)

Powered by Discuz! X3.4