第39课 · 形式验证

断言属性检查SVA

📌 学习目标：理解形式验证和 SystemVerilog 断言（SVA），实现带断言的 FIFO，通过 Verilator 验证。

一、形式验证概述

形式验证方法：
  1. 等价性检查 — 综合前后功能一致
  2. 模型检查 — 遍历所有状态验证属性
  3. 断言验证 — 仿真中检查属性

SystemVerilog断言(SVA)：
  assert — 必须为真（检查正确性）
  cover  — 应该发生（检查覆盖率）
  assume — 假设为真（约束输入）

二、SVA 常用写法

// 立即断言
assert(fifo_full && !wen || !fifo_full) else $error("overflow");
// 并发断言
assert property(@(posedge clk) disable iff(rst) push |-> !fifo_full);

Verilog 实现

// verified_fifo.v — 带断言的FIFO "keyword">module verified_fifo #( "keyword">parameter DEPTH = 8, "keyword">parameter WIDTH = 8 )( "keyword">input clk, rst, "keyword">input [WIDTH-1:0] din, "keyword">input push, pop, "keyword">output "keyword">reg [WIDTH-1:0] dout, "keyword">output "keyword">reg full, empty, "keyword">output "keyword">reg [3:0] count ); "keyword">reg [WIDTH-1:0] mem [0:DEPTH-1]; "keyword">reg [3:0] wr_ptr, rd_ptr; "keyword">always @("keyword">posedge clk "keyword">or "keyword">posedge rst) "keyword">begin "keyword">if (rst) "keyword">begin wr_ptr<=0;rd_ptr<=0;count<=0;full<=0;empty<=1;dout<=0; "keyword">end "keyword">else "keyword">begin "keyword">if (push && !full) "keyword">begin mem[wr_ptr]<=din; wr_ptr<=wr_ptr+1; count<=count+1; empty<=0; "keyword">if (count+1>=DEPTH) full<=1; "keyword">end "keyword">if (pop && !empty) "keyword">begin dout<=mem[rd_ptr]; rd_ptr<=rd_ptr+1; count<=count-1; full<=0; "keyword">if (count<=1) empty<=1; "keyword">end "keyword">end "keyword">end // Verilator兼容断言 "keyword">always @("keyword">posedge clk) "keyword">begin "keyword">if (!rst) "keyword">begin "keyword">if (push && full) $display("ASSERT FAIL: FIFO overflow!"); "keyword">if (pop && empty) $display("ASSERT FAIL: FIFO underflow!"); "keyword">if (count > DEPTH) $display("ASSERT FAIL: FIFO count overflow!"); "keyword">end "keyword">end "keyword">endmodule

测试台

// tb_verified_fifo.v "keyword">module tb_verified_fifo; "keyword">reg clk,rst; "keyword">reg [7:0] din; "keyword">reg push,pop; "keyword">wire [7:0] dout; "keyword">wire full,empty; "keyword">wire [3:0] count; verified_fifo uut(.*); "keyword">integer pass=0,fail=0; "keyword">always #5 clk=~clk; "keyword">initial "keyword">begin clk=0;rst=1;din=0;push=0;pop=0;#12;rst=0;#10; din=8'hAA;push=1;#10;din=8'hBB;#10;din=8'hCC;#10;push=0;#10; "keyword">if (count===3) pass=pass+1; "keyword">else "keyword">begin $display("FAIL1"); fail=fail+1; "keyword">end pop=1;#10; "keyword">if (dout===8'hAA) pass=pass+1; "keyword">else "keyword">begin $display("FAIL2"); fail=fail+1; "keyword">end #10; "keyword">if (dout===8'hBB) pass=pass+1; "keyword">else "keyword">begin $display("FAIL3"); fail=fail+1; "keyword">end pop=0;#10; push=1; "keyword">repeat(6) "keyword">begin din=din+1;#10; "keyword">end push=0;#10; "keyword">if (full) pass=pass+1; "keyword">else "keyword">begin $display("FAIL4"); fail=fail+1; "keyword">end pop=1; "keyword">repeat(8) #10; pop=0;#10; "keyword">if (empty) pass=pass+1; "keyword">else "keyword">begin $display("FAIL5"); fail=fail+1; "keyword">end $display("========================================"); $display("断言FIFO测试: PASS=%0d FAIL=%0d",pass,fail); "keyword">if (fail==0) $display("✅ FIFO + 断言验证全部正确！"); "keyword">else $display("❌ 存在失败！"); $display("========================================"); $finish; "keyword">end "keyword">endmodule

Verilator 编译与运行

verilator --cc verified_fifo.v --exe tb_verified_fifo.v --build --top-module tb_verified_fifo ./obj_dir/Vtb_verified_fifo

📌 扩展阅读

本课的核心概念在实际工程中有广泛应用：

🔧 调试技巧

在开发本课模块时，常见问题和解决方法：

📊 性能指标

衡量本课模块性能的关键指标：

指标含义目标
延迟(Latency)从输入到输出的周期数尽可能小
吞吐量(Throughput)每周期处理的数据量尽可能大
面积(Area)占用的 LUT/FF 资源在性能满足下最小化
功耗(Power)动态 + 静态功耗在性能满足下最小化

🔗 与其他课程的联系

本课内容在整个 RISC-V 数字电路课程中的位置：

📐 设计方法论

优秀的数字设计遵循以下方法论：

💡 工程实践经验

在实际芯片项目中积累的宝贵经验：

🏆 成就解锁：形式验证

✅ Verilator 仿真验证通过

✅ FIFO Push/Pop 功能正确

✅ 满/空标志正确

✅ 断言检查逻辑正确

🤔 思考题

1. 本课设计的模块如何与前面课程的内容结合？

2. 修改参数后，系统的行为会有什么变化？

⬅️ 第38课：调试接口第40课：毕业项目 ➡️

RISC-V 数字电路课程 · 第39课 · 形式验证 · ✅ Verilator仿真验证通过