✅ 断言与功能覆盖：PSL 与 SVA

这一篇在干嘛？

在 HDL 代码中使用断言（Assertion）可以显著提升设计的「可观测性」，让错误自己浮出水面，而不是等你在几百万行的波形里大海捞针。这一篇对应官方 Tutorial 的第 14 章（PSL 断言）和第 15 章（SystemVerilog 断言与功能覆盖）：我们先不加断言跑一遍仿真、体会排查有多痛苦；再加上断言重跑，看它如何把报错时间提前 80 倍；最后用功能覆盖（Functional Coverage）回答一个更难的问题——「我的测试到底测全了没有」。

PSL 断言：用设计意图自动抓错（对应原文第 14 章）

断言是什么，为什么值得用

断言（Assertion）是对「设计意图」的简单声明：它描述的是接口或设计的假设，例如「刷新请求发出后，最多 14 个周期内必须开始刷新」。QuestaSim 支持用 PSL（Property Specification Language，属性规范语言）编写断言，用于动态仿真验证。断言既可以嵌在 HDL 代码里，也可以放在独立的外部文件中——本例用的是外部文件，好处是不用改动设计代码本身。

实验设计：一个会自我检查的 DRAM 控制器

本节示例是一个 DRAM 行为模型加自检查测试平台（self-checking test bench）。DRAM 控制器位于系统处理器与 DRAM 之间，需要周期性刷新，支持读、写、刷新三种操作。刷新操作优先级最高，但不会抢占正在进行的操作。

示例工程位于（Verilog 与 VHDL 两个版本，本文练习用 Verilog 版）：

• Verilog：<install_dir>/examples/tutorials/psl/verilog/modeling/dram_controller
• VHDL：<install_dir>/examples/tutorials/psl/vhdl/modeling/dram_controller

FPGA 语境

用安路 TD 做设计的同学，通常在 TD 里综合布局，而行为级仿真放在 Questa 这类工具里做。把断言写成独立文件，意味着你不需要改动从 FPGA 工程导出的 RTL，就能给接口加上各种自动检查。

不加断言：错误要到 267400 ns 才暴露

先体会一下没有断言的世界。

1. 新建一个工作目录，把上面示例目录中的所有文件复制进去（避免多人共用示例目录互相干扰）。
2. 启动 QuestaSim：在 UNIX shell 输入 vsim，或双击 Windows 图标；如果弹出 Welcome 对话框，点 Close 关闭。
3. 选择 File > Change Directory，切换到第 1 步创建的目录。
4. 在命令提示符输入：

do run_nopsl.do

这个 DO 文件会依次完成：创建工作库 → 编译设计文件与断言 → 优化设计 → 加载（elaborate）设计 → 运行仿真。可以打开该文件看看内容：优化步骤中的 vopt +acc tb -o dram_opt 命令让所有设计单元在调试时保持可见，并生成名为 dram_opt 的优化文件；加载阶段的 -nopsl 参数则指示编译器忽略 PSL 断言。

运行结果（Verilog 版）是在 267400 ns 报错，停在 dramcon_sim.v 模块的第 266 行（VHDL 版则是 246800 ns、dramcon_sim.vhd 实体第 135 行）。错误信息表明：从内存读出的值与期望值不匹配，控制器工作不正常：

Transcript
#
# ERROR at time 267400:
# Controller is not working
# data written = 01
# data read = 80
#
# ** Note: $stop : dramcon_sim.v(266)
# Time: 267400 ns Iteration: 1 Instance: /tb
# Break in Task readmem at dramcon_sim.v line 266
VSIM 34>]
Now: 267,400 ns Delta: 1 sim:/tb/#INITIAL#92

此时你想找到根因，通常只能：检查波形、找出对该内存地址的所有写操作、核对每次写之后总线上的数据和内存实际内容；如果还没头绪，再去检查所有刷新周期，看是不是某次刷新破坏了这个地址。这些活可能全都要干一遍——取决于你的经验（或者运气），总之是个枯燥的体力活。

5. 选择 Simulate > End Simulation 结束本次仿真。

加载断言：失败时间提前到 3100 ns

现在重新加载设计，并打开断言失败跟踪（assertion failure tracking），看看断言能帮我们省多少事。

1. 在命令提示符输入：

vsim -msgmode both -assertdebug dram_opt

• -msgmode both：把消息同时输出到 Transcript 和 WLF 文件；
• -assertdebug：为调试失败的断言提供额外的调试环境（后面会用到 Assertion Debug 面板）；
• dram_opt：就是上一次运行时优化生成的文件名。

2. 修改 WildcardFilter 设置，执行：

set WildcardFilter "Variable Constant Generic Parameter SpecParam Memory Endpoint CellInternal ImmediateAssert"

不改 WildcardFilter，断言信号看不见

这条命令把 Assertion、Cover、ScVariable 从默认的通配过滤列表中移除了。默认情况下这三类对象会被过滤器挡掉，不会被仿真器记录（log），你在波形窗口里根本看不到它们。想让断言、Cover 指令、SystemC 变量进入调试环境，这一步必不可少。

3. 打开 Assertions 窗口查看所有 PSL 断言：输入 view assertions（也可以通过主菜单 View > Coverage > Assertions 开关该窗口；窗口太小时可自行调整大小）：

Name	Assertion Type	Language	Enable	Failure Count	Pass Count
/tb/assert_test_read_response	Concurrent	PSL	on	0	0
/tb/assert_test_write_response	Concurrent	PSL	on	0	0
/tb/assert_check_as_deasserts	Concurrent	PSL	on	0	0
/tb/cntrl/assert_check_refresh	Concurrent	PSL	on	0	0
/tb/cntrl/assert_refresh_rate	Concurrent	PSL	on	0	0
/tb/cntrl/assert_check_write	Concurrent	PSL	on	0	0
/tb/cntrl/assert_check_read	Concurrent	PSL	on	0	0

每个断言都有失败计数（Failure Count）和通过计数（Pass Count），类型为 Concurrent（并发断言，随时钟持续检查）。

4. 把所有断言设置为「失败即中断」： a. 点击 Assertions 窗口使其成为活动窗口； b. 选择主菜单 Assertions > Configure，打开 Configure Assertions 对话框； c. 在 Change on 区选择 All assertions； d. 在 Enable 区选择 On； e. 在 Action 区选择 Break——任何断言失败都会让仿真停下来； f. 在 Passes Logging 区选择 On； g. 点 OK 关闭对话框。

以上操作的命令行等价写法：

assertion action -cond fail -exec break -r *
assertion pass -log on -r *

5. 把断言信号加入 Wave 窗口：在 Assertions 窗口全选所有断言 → 右键弹出菜单 → 选 Add Wave > Selected Objects。Wave 窗口中，断言信号以品红色三角形标注：

6. 输入 run -all 运行仿真。这一次，Assertions 窗口中 assert_check_refresh 被高亮，Failure Count 列显示 1：

Name	Assertion Type	Language	Enable	Failure Count	Pass
/tb/assert_test_read_response	Concurrent	PSL	on	0
/tb/assert_test_write_response	Concurrent	PSL	on	0
/tb/assert_check_as_deasserts	Concurrent	PSL	on	0
/tb/cntrl/assert_check_refresh	Concurrent	PSL	on	1
/tb/cntrl/assert_refresh_rate	Concurrent	PSL	on	0
/tb/cntrl/assert_check_write	Concurrent	PSL	on	0
/tb/cntrl/assert_check_read	Concurrent	PSL	on	0

Transcript 显示 dram_cntrl.psl 文件中的 assert_check_refresh 断言在 3100 ns 失败，仿真就停在这一刻。对比一下：不加断言时，测试平台要到 267400 ns 才报错——加断言后，报错所需的仿真时间缩短了 80 多倍（VHDL 版：3800 ns 报错，对比 246800 ns，缩短 60 多倍）。

# ** Note: Assertion passed
# Time: 2800 ns Started: 2100 ns Scope: /tb/assert_check_as_deasserts File: dram tb.psl Line: 21
# ** Error: Assertion failed
# Time: 3100 ns Started: 2700 ns Scope: /tb/cntrl/assert_check_refresh File: dram_cntrl.psl Line: 24 Expr: (cas_n~|ras_n)&we_n
# ** Note: Requesting simulation stop on assertion event
# Time: 3100 ns Scope: /tb/cntrl/assert_check_refresh File: dram_cntrl.psl Line: 24
# Simulation stop requested.
VSIM 13>

7. 点击 dram_cntrl.psl 标签打开 Source 窗口：蓝色箭头指向仿真停止的位置——第 24 行的 check_refresh 断言。
8. 点击 Wave 标签打开波形窗口：仿真中断点出现一个红色三角形，assert_check_refresh 断言的值一栏显示 FAIL（绿色三角形表示断言通过；断言波形中蓝色段表示断言未激活，绿色段表示激活中）。

断言调试面板：直接给出「嫌疑信号」

由于加载时用了 -assertdebug 参数，还可以在 Wave 窗口的 Assertion Debug 面板里查看失败断言的细节：选择 Wave > Assertion Debug。

Verilog 版显示 assert_check_refresh 失败，断言起始时间（Start Time）为 2700 ns，并且 Signals of Interest（相关信号）列直接列出了导致失败的信号：

VHDL 版同样显示该断言失败，Start Time 为 2900 ns：

Signals of Interest 列显示的正是造成断言失败的信号——调试范围一下子从「整个设计」缩小到「这几个信号」。

读懂 PSL：把那条失败的断言逐字拆开

先看失败断言的源码（dram_cntrl.psl）：

C:/Tutorial/examples/tutorials/psl/verilog/modeling/dram_controller/dram_cntrl.psl (/tb/cntrl) - Default
Ln#
sequence refresh_sequence =
    {~cas_n & ras_n & we_n; [*1]; (~cas_n & ~ras_n & we_n)[*2]; cas_n & ras_n};
property check_refresh = always ( {rose(refresh)} | ->
    {(mem_state != IDLE)[*0:14]; (mem_state == IDLE); refresh sequer abort fell(reset_n));
assert check_refresh;
// declare refresh rate check
sequence signal_refresh = {[*24]; rose(refresh)};
property refresh_rate = always ( {rose(reset_n) || rose(refresh)} |=> 
{signal_refresh} abort fell(reset_n));

逐条解释这些语法：

• sequence ... = { ... };：序列（sequence），描述「按周期依次排列的一串布尔条件」。分号分隔不同周期：第一周期满足 ~cas_n & ras_n & we_n，第二周期为 [*1]（任意一个周期），接着 (~cas_n & ~ras_n & we_n)[*2] 表示该条件连续重复 2 个周期，最后 cas_n & ras_n。其中 ~ 是按位取反，& 是按位与，| 是按位或。刷新协议的关键是：整个刷新过程中 we_n（写使能，低有效）必须保持为高，即写使能不激活。
• property check_refresh = always ( ... );：属性（property）。always 表示「每一个时钟周期都持续检查括号内的内容」。
• {rose(refresh)} |-> { ... }：蕴含（implication）。rose(refresh) 表示 refresh 信号出现上升沿；|-> 是重叠蕴含——左边序列在当前周期成立时，右边的序列立即（同周期）开始检查。与之相对的 |=> 是非重叠蕴含，右边从下一个周期才开始检查。
• {(mem_state != IDLE)[*0:14]; (mem_state == IDLE); refresh_sequence}：右边序列的含义是——mem_state 不等于 IDLE 的情况最多重复 14 个周期（[*0:14] 表示重复 0 到 14 次，对应「一次读或写最长 14 个周期；若控制器已处于 IDLE，则等待 0 个周期」），然后必须到达 IDLE 状态，并且下一个周期开始刷新序列 refresh_sequence（定义在第 18 行）。
• abort fell(reset_n)：中止子句。一旦 reset_n 出现下降沿（fell，即复位有效），就放弃当前的检查——复位期间不检查协议是合理的。
• assert check_refresh;：把属性声明为断言，仿真器会在每个周期检查它。
• sequence signal_refresh = {[*24]; rose(refresh)};：任意 24 个周期之后必须出现一次 refresh 上升沿，用于检查刷新率（refresh_rate 属性）。

这段属性翻译成人话就是：当 refresh 信号有效时，等控制器回到 IDLE（最多等 14 个周期），下一个周期就必须开始刷新序列；整个刷新期间 we_n 必须保持无效（高电平）。

顺藤摸瓜：we_n 在 REF2 状态被拉低了

断言只告诉我们「刷新协议被违反了」，接下来要找出是谁违反的。

1. 检查 we_n 是否贯穿 REF1 和 REF2 两个状态都保持为高： a. 在 Wave 窗口展开 assert__check_refresh，显示断言引用的所有信号； b. 缩放并滚动波形，同时观察 we_n 和 mem_state：

一眼就能看出问题：we_n 只在 REF1 状态为高，到了 REF2 状态就变低了——这正是断言失败的原因。继续深挖。

2. 在 Dataflow 和 Source 窗口检查 we_n 的驱动来源： a. 选择 View > Dataflow 打开数据流窗口，并点击它确保激活，菜单栏会出现 Dataflow 菜单； b. 选择 Dataflow > Dataflow Preferences > Options 打开 Dataflow Options 对话框（若 Dataflow 窗口未停靠，则从其窗口菜单选 Tools > Options）； c. 取消勾选 Show Hierarchy，点 OK：

d. 在 Wave 窗口选中写使能信号 we_n； e. 选择 Add > To Dataflow > Selected Items。

Verilog 版：Dataflow 窗口显示 we_n 由 #ASSIGN#104 进程驱动，输入是 rw 和 mem_state。黄色标注的数值是仿真停止时刻（3100 ns）各信号的取值：mem_state 为 REF2 时 we_n 是 St0，而它本应是 St1——失败原因确认：

如果 we_n 显示的不是 St0，可在 VSIM> 提示符输入 radix -symbolic 命令切换为符号显示。

VHDL 版：Dataflow 窗口显示 we_n 由第 61 行的进程驱动，输入同样是 rw 和 mem_state，停止时刻为 3800 ns：mem_state 为 REF2 时 we_n 为 0，本应为 1：

f. 双击驱动 we_n 的 #ASSIGN#104 进程（VHDL 中为 line_61），在 Source 窗口打开其源码。

3. 找到 Bug。Verilog 版源码停在 dramcon_rtl.sv 第 104 行——给 we_n 赋值的逻辑没有考虑 REF2 状态：

// Deassert we_n high during refresh
`ifdef BUG
| assign #'DEL we_n = rw | (mem_state == REF1);
`else
assign #'DEL we_n = rw | (mem_state == REF1)
| (mem_state == REF2);
`endif

可以看到错误赋值就在 ifdef BUG 分支里，紧随其下（106-107 行）的正确赋值会让 we_n 在刷新周期的两个状态（REF1 与 REF2）都保持高电平。

VHDL 版停在 dramcon_rtl.vhd 第 61 行，同样是赋值逻辑漏掉了 REF2 状态，正确写法在第 65 行：

例 1
    tutorial/examples/tutorials/psl/vhdl/modeling/dram_controller/dramcon_rtl.vhd (/tb/cntrl/withbug) - Default
    Ln#
    -- Deassert we_n high during refresh
    withbug : if BUG generate
    we_n <= '1' when (rw = '1') or (mem_state = REF1) else '0'.
    end generate;
    nobug : if not BUG generate
    we_n <= '1' when (rw = '1') or (mem_state = REF1) or (mem_
    end generate;

本章收尾

1. 恢复 WildcardFilter 出厂默认设置：

set WildcardFilter "default"

2. 选择 Simulate > End Simulation 结束当前仿真，点 Yes。

SVA 断言与功能覆盖：从「抓错」到「测全」（对应原文第 15 章）

这一章用 SystemVerilog 断言（SVA）和功能覆盖做一个循序渐进的功能验证入门。流程与上一章类似：先关掉断言跟踪跑一遍、记录多久才撞上错误；再打开断言重跑、体会定位速度；然后用 cover 指令与 covergroup 让测试平台「活」起来并统计功能覆盖率；最后用图形界面生成覆盖率报告。

交织器设计：数据被怎样打乱

示例是一个交织器（Interleaver）设计。交织器把输入数据的字节顺序打乱，以辅助 Reed Solomon/Viterbi 之类的检错纠错方案。本设计中，输入数据由一个同步字节（0xb8 或 0x47）加 203 字节组成，其中 187 字节是有效载荷数据（payload），16 字节是 Reed Solomon 编码器预先附加的数据：

同步字节	187 字节有效载荷数据	16 字节 RS 编码

交织器有 12 个层级（level），编号 0 到 11。除第一级外，每一级在概念上都可以看作一个 FIFO 移位寄存器，深度比上一级大 17：level 0 深度为 0，level 1 为 17，level 2 为 34，以此类推，level 11 为 187。数据包的同步字节走 level 0；当一个字节装入某级的 FIFO 移位寄存器时，该级移出的字节就是交织器的输出。

这些 FIFO 移位寄存器实际上是用一块 2K×8 的 RAM 实现的：RAM 划分为 11 个区段，每级有独立的读、写地址寄存器，由一个状态机控制当前读写的是哪一级，并选择哪一级的地址寄存器驱动 RAM 的实际地址输入。一个公共模块 rdy_acpt 负责收发交织器的数据输入（di）与数据输出（do）端口，实现简单的握手协议：上游把数据驱动到交织器并置位 ready 信号（di_rdy），且必须保持数据和 rdy 直到下游应答（di_acpt）；也就是说，只有 rdy 和 acpt 在时钟上升沿同时有效，数据才算传送完成。握手协议的两端都遵守这一规则。

测试平台：事务级激励 + 记分板

测试平台的组件连接如下：激励生成器（stimulus generator）产生随机数据包送给驱动器（driver）。虽然测试平台是基于模块的，激励生成器产生的仍是事务级（transaction-based，SV 类）数据包——这正是高级验证方法学（AVM）的优势：不必把测试平台改造成完全的面向对象环境，也能享受事务级建模（TLM）的好处。

各组件分工：

• driver（驱动器）：把 TLM 数据包转成引脚级（pin-level）信号，并用随机化改变数据包送达器件的时序；
• monitor（监视器）：把 DUT 输入输出引脚上的活动还原成事务，供覆盖率收集器和记分板使用；
• scoreboard（记分板）：内含交织器的「黄金」参考模型，与器件实际输出比对；还有一条反馈回路，告诉激励生成器何时测试完成；
• coverage collector（覆盖率收集器）：累积功能覆盖信息，帮助判断测试是否充分，比如统计数据包送达时用了多少种不同的延迟值；
• responder（应答器）：本例中其实是 driver 的一部分，提供数据包传送所需的 ready/accept 握手信号。

示例文件位于：/<install_dir>/examples/tutorials/systemverilog/vlog_dut。

不加断言：TEST FAILED，但不知从何查起

1. 新建目录，把上面的示例文件复制进去。
2. 如有必要启动 QuestaSim（输入 vsim 或用 Windows 图标），选择 File > Change Directory 切换到新目录。
3. 在 Questa SIM> 提示符输入：

do assert.do

这个 DO 文件会编译并加载设计、在不启用断言的情况下运行仿真，然后暂停（Windows 下可能弹出 Finish Vsim 对话框问是否结束，点 No）。稍后我们会输入 resume 命令，重新在启用断言的情况下运行。

设计加载后，第一次仿真一直跑到 top.sv 模块中的 $finish，Transcript 窗口显示 Test Failed。摘要显示记分板正确收到了 22 个数据包——这是自检查测试平台的典型输出：

# ** MESSAGE: interleaver_score.svh(29) @ 474630: env.scoreboard [Upstream Packet Received by Scoreboard] b8 460090 474630
# ***************************
# * # #
# * # #
# * # TEST FAILED *
# * # #
# * # #
# ***************************
# Individual failure points recorded by:
# ** Note: $finish : top.sv(25)
# Time: 474650 ns Iteration: 1 Instance: /top
# 1
# Break in Module top at top.sv line 25
# MACRO ./assert.do PAUSED at line 21
VSIM(pauSED)>

这时候你照常会去生成波形来排查，但波形并不能清楚地指出问题源头——从哪里下手？如果没有断言这类调试工具，这可能是个非常难缠的问题。

加断言：让仿真停在出错的那一拍

1. 在 Transcript 窗口的 VSIM(paused)> 提示符输入 resume，让仿真带着断言重新运行。
2. 设计加载后，把所有断言配置为「失败即中断」： a. Assertions 窗口应已打开；若没有，选择 View > Coverage > Assertions。注意每条断言的 Pass 和 Failure 都已启用——意味着通过和失败都会计数、都会在 Wave 窗口留下标记。这不是默认行为，必须像本例那样用 vsim -assertdebug 开关启动仿真才能得到（该命令写在 assert.do 文件里）； b. 点击 Assertions 标签或窗口标题栏使其激活，菜单栏出现 Assertions 选项； c. 确保没有选中任何断言（Edit > Unselect All）； d. 执行：

assertion action -cond fail -exec break -r *

Assertions 窗口的 FPSA Action 列变为 BCCC，其中第一个字母 B 表示任何断言失败都会 Break（中断）。FPSA 代表 Failures（失败）、Passes（通过）、Starts（线程启动）、Antecedents（前件），这一列的四个字母依次对应这四类事件的动作，可选动作有 Continue（继续）、Break（中断）、Exit（退出）和 TCL（执行 Tcl 命令）。如果窗口里看不到 FPSA Action 列，点击列标题栏左端的下拉箭头，在 Configure Columns 菜单里勾选 FPSA Action 即可：

Assertions
Name	Assertion Type	Language	Enable	Failure Count	FPSA Actions
+ /top/pins_if/di_handshake	Concurrent	SVA	on	0	BCCC
+ /top/pins_if/do_handshake	Concurrent	SVA	on	0	BCCC
+ /top/pins_if/di_data_hold	Concurrent	SVA	on	0	BCCC
+ /top/pins_if/do_data_hold	Concurrent	SVA	on	0	BCCC
+ /top/dut/assert_pkt_start_check	Concurrent	SVA	on	0	BCCC
+ /top/dut/assert_pkt_length_check	Concurrent	SVA	on	0	BCCC
+ /top/dut/assert_sync_bypass_check	Concurrent	SVA	on	0	BCCC
+ /top/dut/fifo/assert_push_mutex_check	Concurrent	SVA	on	0	BCCC
+ /top/dut/fifo/assert_ram_write_check	Concurrent	SVA	on	0	BCCC
+ /top/dut/fifo/assert_ram_write_check_1	Concurrent	SVA	on	0	BCCC

3. 把与 /top/dut/fifo 相关的所有断言加入 Wave 窗口： a. 在 Assertions 窗口选中 /top/dut/fifo/assert_push_mutex_check； b. 按住 Shift 键再点选 /top/dut/fifo/assert_ram_read_check_10，则与 fifo 相关的所有断言都被选中（蓝色高亮）； c. 选择主菜单 Add > To Wave > Selected Objects，选中的断言出现在 Wave 窗口：

Wave		Msgs
+	Interleave DUT
+	assert_push_mutex_check	INACTIVE
+	assert_ram_write_check	INACTIVE
+	assert_ram_write_check_1	INACTIVE
+	assert_ram_write_check_2	INACTIVE
+	assert_ram_write_check_3	INACTIVE
+	assert_ram_write_check_4	INACTIVE

断言触发后：run 0 的小秘密

1. 在 Transcript 窗口的 Questa SIM 提示符输入 run -all；当仿真器停下后，再输入：

run 0

为什么断言设为 Break 之后还必须补一条 run 0？这是调度机制决定的：「break」必须发生在活动事件队列（active event queue）里，而断言消息被调度在观察区（observed region）——它位于同一时间步中更靠后的位置。run 0 会把仿真推进到当前时间步的末尾，让断言消息得以打印出来。

2. 查看 Transcript 输出。注意断言失败消息直接给出了失败的表达式——这是 -assertdebug 开关带来的功能（命令写在 assert.do 文件里）：

# ** MESSAGE: interleaver_score.svh(29) @ 198090: env.scoreboard [Upstream Packet Received by Scoreboard] b8 183330 198090
# ** MESSAGE: interleaver_stimulus.svh(37) @ 198110: env.stimulus [Stimulus Generator sending packet to Driver] 184
# ** Note: Requesting simulation stop on assertion event
# Time: 198130 ns Scope: top.dut.fifo File: fifo_shift_ram.v Line: 44
# Simulation stop requested.
VSIM 8> run 0
# ** Error: Assertion error.
# Time: 198130 ns Started: 198110 ns Scope: top.dut.fifo File: fifo_shift_ram.v
Line: 44 Expr: waddr[11]<=1722

3. 在 Assertions 窗口查看失败断言：失败的断言被高亮，其 Failure Count 列显示 1：

Assertions
Name	Assertion Type	Language	Enable	Failure Count	P
+ - ▲ /top/dut/fifo/assert_ram_write_check_8	Concurrent	SVA	on	0
+ - ▲ /top/dut/fifo/assert_ram_write_check_9	Concurrent	SVA	on	0
+ - ▲ /top/dut/fifo/assert ram write check…	Concurrent	SVA	on	1
+ - ▲ /top/dut/fifo/assert ram_read_check	Concurrent	SVA	on	0
+ - ▲ /top/dut/fifo/assert ram_read_check_1	Concurrent	SVA	on	0
+ - ▲ /top/dut/fifo/assert ram_read_check_2	Concurrent	SVA	on	0

4. 检查 fifo_shift_ram.v 源码视图（该标签页应已打开）。仿真停在第 44 行，因为该行断言失败了，蓝色箭头指向它：

C:/Tutorial/examples/tutorials/systemverilog/vlog_dut/fifo_shift_ram.v (/top/dut/fifo) - Default
Ln#
40 assert property (ram_write_check(push[6], waddr[7], 11'd640, 11'd758));
41 assert property (ram_write_check(push[7], waddr[8], 11'd768, 11'd903));
42 assert property (ram_write_check(push[8], waddr[9], 11'd1024, 11'd1176))
43 assert property (ram_write_check(push[9], waddr[10], 11'd1280, 11'd1449))
44 assert property (ram_write_check(push[10], waddr[11], 11'd1536, 11'd1722))

参数化的 property 定义从第 29 行开始，在源码视图中滚动过去：

property ram_write_check (we, waddr, lorange, hirange);
@(posedge clk) we |-> ((addra == waddr && waddr >= lorange && waddr <= hirange
(!we && waddr >= lorange && waddr <= hirange));
endproperty

逐条解读这条 SVA 属性：

• property ram_write_check (we, waddr, lorange, hirange);：带四个参数的属性，可复用于 11 个层级，只需传入不同的写使能、写地址和合法地址范围；
• @(posedge clk)：时钟采样事件，所有检查都同步在时钟上升沿；
• we |-> ( ... )：又是蕴含——当 we（本例中即 push[10]）有效时，同一个时钟周期立即检查后面的表达式；
• 蕴含右侧第一段：RAM 地址总线 addra 必须等于 level 11 的写地址总线 waddr[11]，且 waddr[11] 必须落在 1536 到 1722 的合法范围内（&& 表示逻辑与，>=/<= 为比较）；
• 蕴含右侧第二段对应下一个周期：we 应被撤销（de-assert），且 waddr[11] 的新值仍在 1536 到 1722 范围内。

5. 点击 Wave 标签，在波形窗口中搜索并查看断言失败点： a. 选择 Edit > Find 调出搜索栏； b. 在搜索栏选择 Search For > Value； c. 在输入框输入 fail，边输入边搜索，FAIL 值会被高亮。

波形视图中的倒置红色三角形表示断言失败位置：

• 绿色「中线」表示断言处于激活状态，低位的蓝线表示未激活；

• 蓝色方块表示断言线程的起点；

• 绿色三角形表示断言通过——只有加载时用了 vsim -assertdebug 开关才会显示通过标记（参见 assert.do 文件）。

  d. 在 Wave 窗口展开 assert_ram_write_check_10 断言（点它旁边的 + 号）并放大； e. 把 addra 和 waddr 的进制改为 Unsigned：同时选中两个信号，右键 → Radix > Unsigned：

此刻 waddr[11] 已经累加到 1723，超出了允许的地址范围——回想 Transcript 里的断言消息，失败表达式正是 waddr[11]<=1722：

Wave - Default		Msgs
	/top/dut/fifo/assert_ram_write_check_10	FAIL
	/top/dut/fifo/clk	1’h1
	/top/dut/fifo/push[10]	1’h0
	/top/dut/fifo/waddr[11]	11’d1723
	/top/dut/fifo/addra	11’d0
	ActiveCount	0
	/top/dut/fifo/assert_ram_read_check	START

6. 在 Dataflow 窗口检查该信号： a. 点击 waddr 信号旁的 + 号展开，滚动到 waddr[11]； b. 选中 waddr[11]，选择 Add > To Dataflow > Selected Items，把它送入 Dataflow 窗口。

waddr[11] 被高亮显示，它所在的块是一个 ALWAYS 过程：

c. 双击 Dataflow 窗口中的 ALWAYS 块，fifo_shift_ram.v 源码视图自动打开，蓝色箭头指向该块对应的代码：

C:/Tutorial/examples/tutorials/systemverilog/vlog_dut/fifo_shift_ram.v (/top/dut/fifo) - Default = (((+) →)
Ln#
132    always @(posedge clk or negedge reset_n)
133    if (!reset_n)
134    begin
135    waddr[1] <= 11'd0;
136    waddr[2] <= 11'd64;
137    waddr[3] <= 11'd128;
138    waddr[4] <= 11'd256;
139    waddr[5] <= 11'd384;
140    waddr[6] <= 11'd512;
141    waddr[7] <= 11'd640;
142    waddr[8] <= 11'd768;
143    waddr[9] <= 11'd1024;
144    waddr[10] <= 11'd1280;
145    waddr[11] <= 11'd1536;
146    end

往下滚动到处理 waddr[11] 的 case 分支：waddr[11] 的复位上限被错误地写成了 11’d1724 而不是 11’d1722——这就是错误根源：

C:/Tutorial/examples/tutorials/systemverilog/vlog_dut/fifo_shift_ram.v (/top/dut/fifo) - De
Ln#
199 default:
200 if (BUG == 0)
201 if (waddr[11] == 11'dl722)
202 waddr[11] <= 11'dl536;
203 else
204 waddr[11] <= waddr[11] + 11'dl;
205 else
206 if (waddr[11] == 11'dl724)
207 waddr[11] <= 11'dl536;
208 else
209 waddr[11] <= waddr[11] + 11'dl;
210 endcase
211

7. 退出仿真：输入 quit -sim。

功能覆盖：错误之外，还要知道「测了多少」

SystemVerilog 的功能覆盖能力让你能在功能层面验证设计——断言告诉你「哪里错了」，覆盖告诉你「哪些情况测过了、哪些还没测到」。

1. 再次加载交织器：在 Questa SIM> 提示符输入：

do fcov.do

fcov.do 里的一个小开关

fcov.do 给 vsim 命令加了 -cvg63 选项，用于保留对每个实例（instance）、coverpoint 和 cross 的单独数据收集，详见 SystemVerilog 2008 的 type_option.merge_instances。

交织器用参数 PKT_GEN_NUM（设为 80）决定要交织的有效数据包数量。记分板收满并校验完 80 个数据包后，会通知测试控制器，控制器随即让激励生成器和驱动器停工。仿真过程中，覆盖率收集器为每个送入和输出的数据包记录多项指标。下面是 up_cvg covergroup 的源码：

(/interleaver_svc_pkg::interleaver_cover::interleaver_cover_1::#up_cvg#)
Ln#
// Upstream packet covergroup
covergroup up_cvg;
option.auto_bin_max = 256;
coverpoint upcov_data;
coverpoint upcov_sync {
bins sync [] = { 71, 184 };
bins illegal = default;
}
coverpoint up_delay {
bins short [] = {{0:4}};
bins sh2med [] = {{5:9}};
bins md2lng [] = {{10:14}};
bins long [] = {{15:19}};
bins vrylng = default;
}
endgroup

这个 covergroup 记录监视器捕获的上游事务信息，包括数据包有效载荷的逐字节取值、同步字节以及每次数据传送的延迟时间：

• option.auto_bin_max = 256：SystemVerilog LRM 默认只自动创建 64 个 bin；这里设为 256，保证每个字节取值都有自己的 bin；
• coverpoint upcov_sync 里的 bins sync [] = { 71, 184 };：两个同步字节的十进制值，对应 8’h47 和 8’hb8；bins illegal = default; 把其他所有取值收进名为 illegal 的 bin——这个 bin 理应始终为空；
• coverpoint up_delay：因为 driver 是随机化驱动的，所以统计有效载荷传送延迟的分布。各 bin 名一目了然：short（04）、sh2med（59）、md2lng（1014）、long（1519），而 vrylng = default 兜底记录 20 周期以上的超长延迟。

2. 输入 run 0——接口在仿真运行前不会显示 covergroup，这一步只是让 Covergroups 窗口能显示它们。
3. 打开 Covergroups 窗口（View > Coverage > Covergroups），点 + 号展开 /top/dut 层次，会看到另外两个监视交织器状态机的 covergroup——sm_transitions_cvg 和 sm_cvg：

Covergroups
Name Coverage Goal % of Goal Status Included
/top/dut/fifo
TYPE ram_cvg 0.0% 100 0.0% ✓
/top/dut
TYPE sm_transitions_cvg 0.0% 100 0.0% ✓
CVP sm_transitions_cvg::int_state... 0.0% 100 0.0% ✓
INST \top/dut/sm_cvg_c1 0.0% 100 0.0% ✓
TYPE sm_cvg 0.0% 100 0.0% ✓
CVP sm_cvg::int_state 0.0% 100 0.0% ✓
CVP sm_cvg::in_hs 0.0% 100 0.0% ✓
CVP sm_cvg::out_hs 0.0% 100 0.0% ✓
CROSS sm_cvg::in_hsXint_state 0.0% 100 0.0% ✓
CROSS sm_cvg::out_hsXint_state 0.0% 100 0.0% ✓
INST \top/dut/sm_cvg_c2 0.0% 100 0.0% ✓

sm_transitions_cvg 记录状态机的合法状态跳转；sm_cvg 检查状态机在正确状态下收发数据。sm_cvg 的源码如下：

atorial/examples/tutorials/systemverilog/vlog_dut/interleaver.sv (/top/dut) - Default
Ln#
92 covergroup sm_cvg @(posedge pins.clk);
93 coverpoint int_state;
94 coverpoint in_hs {
95 bins valid = {1};
96 //ignore_bins invalid = default;
97 }
98 coverpoint out_hs {
99 bins valid = {1};
100 //ignore_bins invalid = default;
101 }
102 in_hsXint_state: cross int_state, in_hs;
103 out_hsXint_state: cross int_state, out_hs;
104 option.at_least = 500;
105 option.comment = "covered it";
106
107 endgroup

解读：

• covergroup sm_cvg @(posedge pins.clk);：covergroup 自带采样事件，每个时钟上升沿采样一次；
• in_hs 与 out_hs 分别由 in_acpt AND in_rdy、out_acpt AND out_rdy 相与得到。状态机在 idle、load_bypass 或 10 个 load 状态中的任一状态时置位 in_acpt，在 send_bypass 或 10 个 send 状态时置位 out_rdy；
• 正常工作时，in_hs 只应在 idle/load_bypass/10 个 load 状态置位，out_hs 只应在 send_bypass/10 个 send 状态置位。把 in_hs 与 int_state、out_hs 与 int_state 做 cross（交叉覆盖），就能验证这一点；
• option.at_least = 500;：每个 bin 至少要命中 500 次才算覆盖完成。

展开 sm_cvg 的 int_state coverpoint 可以看到所有 bin，bin 的值直接显示枚举状态名：

Covergroups
	Name	Coverage	Goal	% of Goal	Status	Included	M
	/top/dut/fifo
	TYPE ram_cvg	0.0%	100	0.0%		√
	/top/dut
	TYPE sm_transitions_cvg	0.0%	100	0.0%		√
	CVP sm_transitions_cvg::int_state	0.0%	100	0.0%		√
	INST Vtop/dut/sm_cvg_c1	0.0%	100	0.0%		√
	TYPE sm_cvg	0.0%	100	0.0%		√
	CVP sm_cvg::int_state	0.0%	100	0.0%		√
	CVP sm_cvg::in_hs	0.0%	100	0.0%		√
	CVP sm_cvg::out_hs	0.0%	100	0.0%		√
	CROSS sm_cvg::in_hsXint_state	0.0%	100	0.0%		√
	CROSS sm_cvg::out_hsXint_state	0.0%	100	0.0%		√
	INST Vtop/dut/sm_cvg_c2	0.0%	100	0.0%		√
	CVP int_state	0.0%	100	0.0%		√
	B bin auto[idle]	0	500	0.0%		√
	B bin auto[send_bypass]	0	500	0.0%		√
	B bin auto[load0]	0	500	0.0%		√
	……（后续 bin 略）

4. 展开 /top/dut/fifo 和 ram_cvg covergroup 的层次。注意 TYPE ram_cvg 包含多个实例（INST 标记）： a. 右键点击 covergroup 名称，在弹出菜单选 View Source 查看其源码：

Covergroups
Name
Coverage Goal % of Goal Status Included M
/top/dut/fifo
TYPE ram_cvg
CROSS ram_cvg::waddrXpush
CVP ram_cvg::add_cp
CVP ram_cvg::we_cp
INST Vtop/dut/fifo/ram_cvg1
INST Vtop/dut/fifo/ram_cvg2
INST Vtop/dut/fifo/ram_cvg3
INST Vtop/dut/fifo/ram_cvg4
INST Vtop/dut/fifo/ram_cvg5
INST Vtop/dut/fifo/ram_cvg6
INST Vtop/dut/fifo/ram_cvg7
INST Vtop/dut/fifo/ram_cvg8
INST Vtop/dut/fifo/ram_cvg9
INST Vtop/dut/fifo/ram_cvg10
View Source
Report...
Hide Covergroup Instances
Use CrossPrintMissing
✓ Show Zero Weight Objects
Test Analysis
XML Import Hint
Filter
Expand
100 0.0%
20 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0.0%
100 0,0%

fifo_shift_ram.v 源码视图随即打开：

Tutorial/examples/tutorials/systemverilog/vlog_dut/fifo_shift_ram.v (/top/dut/fifo) - Default
Ln#
68 covergroup ram_cvg (int idx, add_low, add_high) @(posedge clk);
69 option.per_instance = 1;
70 //option.goal = 10;
71 //option.cross_num_print_missing = 1;
72 we_cp: coverpoint push[idx-1] {
73 option.goal = 10;
74 bins valid = { 1 };
75 ignore_bins inval = { 0 };
76 }
77
78 add_cp: coverpoint waddr[idx] {
79 option.goal = 20;
80 type_option.goal = 20;
81 bins valid_addr[] = {{add_low:add_high}};
82 }
83 waddrXpush: cross add_cp, we_cp;
84 endgroup

由于交织器各层级由一块 RAM 实现、每级占据不同的 RAM 地址区间，这个 covergroup 用来验证读写都只发生在合法地址上。注意：只有一个 covergroup 定义，却有 11 个实例——每个实例用不同的构造参数创建：

Tutorial/examples/tutorials/systemverilog/vlog_dut/fifo_shift_ram.v (/top/dut/fifo) - Default
Ln#
85
86	ram_cvg ram_cvg1 = new(1,0,16);
87	ram_cvg ram_cvg2 = new(2,64,97);
88	ram_cvg ram_cvg3 = new(3,128,178);
89	ram_cvg ram_cvg4 = new(4,256,323);
90	ram_cvg ram_cvg5 = new(5,384,468);
91	ram_cvg ram_cvg6 = new(6,512,613);
92	ram_cvg ram_cvg7 = new(7,640,758);
93	ram_cvg ram_cvg8 = new(8,768,903);
94	ram_cvg ram_cvg9 = new(9,1024,1176);
95	ram_cvg ram_cvg10 = new(10,1280,1449);
96	ram_cvg ram_cvg11 = new(11,1536,1722);
97

因为 covergroup 里有 option.per_instance = 1;，仿真器会为每个实例单独建一个 covergroup，各自只覆盖构造时传入的取值范围；而 TYPE ram_cvg 是所有实例取值的并集。

5. 打开 Cover Directives 窗口查看 cover 指令的源码： a. 若窗口未打开，选择 View > Coverage > Cover Directives。

Cover Directives 标签里只有一条 cover 指令：

Cover Directives
Name	Language	Enabled	Log	Count	AtLeast	Limit	Weight	Cmplt %
/top/dut/cover_s_interleave_sm	SVA	√	Off	0	1	Unlim…	1	0*

b. 右键该指令选 View Source。可见这条 cover 指令同样在跟踪交织器状态机的跳转：

C:/Tutorial/examples/tutorials/systemverilog/vlog_dut/interleaver.sv (/top/dut) - Default
Ln#
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
 
cover property (s_interleave_sm);
 
covergroup sm_transitions_cvg @(posedge pins.clk);
coverpoint int_state {
    bins idle_st = (idle => send_bypass[->1] => load0[->1] => send0[->1] =>
    load1[->1] => send1[->1] => load2[->1] => send2[->1] =>
    load3[->1] => send3[->1] => load4[->1] => send4[->1] =>
    load5[->1] => send5[->1] => load6[->1] => send6[->1] =>
    load7[->1] => send7[->1] => load8[->1] => send8[->1] =>
    load9[->1] => send9[->1] => load10[->1] => send10[->1]);
    bins bypass_st = (load_bypass => send_bypass[->1] => load0[->1] => send0[->1] =>
    load1[->1] => send1[->1] => load2[->1] => send2[->1] =>
    load3[->1] => send3[->1] => load4[->1] => send4[->1] =>
    load5[->1] => send5[->1] => load6[ ->1 ] => send6[->1 ] =>
    load7[->1] => send7[->1] => load8[->1 ] => send8[->1 ] =>

SystemVerilog 提供了多种覆盖设计中重要目标的方式。cover 指令的优势是有时间维度——Questa 的 Wave 窗口能显示指令在何时被命中；covergroup 则无法确定事件被覆盖的精确时刻，但通常更擅长统计数据取值。两者结合：用 cover 指令的时间特性决定「何时」采样，用 covergroup 采样「什么数据」，就构成了强大的组合。

6. 把 cover 指令加入 Wave 窗口两次： a. 回到 Cover Directives 窗口，右键 /top/dut/cover__s_interleave_sm，选 Add Wave > Selected Functional Coverage； b. 重复步骤 a。
7. 运行仿真并查看功能覆盖信息： a. 修改 WildcardFilter，允许记录 cover 指令——下列命令的列表中不含默认被过滤的 Cover 一词（原文此处排版截断为 Assertion Endpoint CellInternal ImmediateAssert，即仍沿用前面 PSL 一节介绍过的 set WildcardFilter 命令，按需增删列表项）； b. 在 Transcript 窗口输入 run -all。设计会一直跑到出现 TEST PASSED 消息（Windows 下若弹出 Finish Vsim 对话框，点 No）。Transcript 显示记分板信息：

# UPSTREAM MONITOR AP PORT WRITE ID= 0 SYNC=b8 START=
# **MESSAGE: interleaver_score.svh(29) @ 1535730: env.scoreboard
# **************************
# *    #    *
# *    #    *
# *    #    TEST PASSED *
# * # #
# *    #
# **************************
# ** Note: $finish : top.sv(25)
#    Time: 1535750 ns Iteration: 2 Instance: /top
# 1
# Break in Module top at top.sv line 25
VSIM 15>

c. 在 Covergroups 窗口展开功能覆盖信息。整体 covergroup 覆盖率接近 95%（见窗口右下角状态栏），但 up_delay covergroup 里有一个 short bin 没有命中——因为目前 driver 在驱动有效载荷数据时，字与字之间至少插入 1 个周期。

另外 sm_cvg 的覆盖率偏低（76.9%），低点集中在 in_hsXint_state 和 out_hsXint_state 两个 cross bin。这是符合预期的：in_hs 只在 idle、load_bypass 或 10 个 load 状态置位，out_hs 只在 send_bypass 或 10 个 send 状态置位，所以这些 cross bin 覆盖缺失恰恰说明设计行为正确，而不是测试不够：

Covergroups
Name	Coverage	Goal	% of Goal	Status	Included
/top/dut/fifo
+ TYPE ram_cvg	100.0%	100	100.0%		√
/top/dut
+ TYPE sm_transitions_cvg	100.0%	100	100.0%		√
INST \top/dut/sm_cvg_c1	100.0%	100	100.0%		√
CVP sm_transitions_cvg::int_state	100.0%	100	100.0%		√
- TYPE sm_cvg	76.9%	100	76.9%		√
+ INST \top/dut/sm_cvg_c2	76.9%	100	76.9%		√
CVP sm_cvg::out_hs	100.0%	100	100.0%		√
CVP sm_cvg::int_state	92.3%	100	92.3%		√
CVP sm_cvg::in_hs	100.0%	100	100.0%		√
- CROSS sm_cvg::out_hsXint_state	46.1%	100	46.1%		√
CROSS sm_cvg::in_hsXint_state	46.1%	100	46.1%		√
/interleaver_svc_pkg/interleaver_cover/interleaver_cover_1
- TYPE up_cvg	98.3%	100	98.3%		√
+ INST \interleaver_svc_pkg::interleaver_cover::interl…	98.3%	100	98.3%		√
+ CVP up_cvg::upcov_sync	100.0%	100	100.0%		√
+ CVP up_cvg::upcov_data	100.0%	100	100.0%		√
……（后续行略）

展开 sm_transitions_cvg 可以看到它记录了 1461 次交织器状态跳转（从 idle 循环开始的 86 次，从 bypass 循环开始的 1375 次）。

d. 打开 Cover Directives 标签。该 cover 指令统计的是同一批状态跳转，因此计数同样是 1461：

Name	Language	Enabled	Log	Count	AtLeast	Limit	Weight	Cmplt
/top/dut/cover_s_interleave_sm	SVA	√	Off	1461	1	Unlim…	1	100

8. 把 Wave 窗口中第二条 cover 指令的视图从 Temporal（时间模式）切换为 Count（计数模式）： a. 右键第二条指令，选 View > Cover Directives > Count Mode：

b. 在 Wave 窗口观察该指令。下面两张截图分别对应两个不同时间点：两张图的上半部分都是指令线程的时间维度视图（线程何时激活），下半部分是实际的计数值。对比两图能直观看到驱动行为的随机性——第一张图里指令线程从开始到结束间隔 1240 ns，下一张图里只有 780 ns：

生成功能覆盖率报告

覆盖率报告既可以通过 GUI 对话框生成，也可以在命令行输入命令完成。

1. 用 GUI 生成报告： a. 在 Cover Directives 窗口空白处右键，选 Report，打开 Functional Coverage Report 对话框； b. 保持 All coverage items 选中，选 Covergroups only； c. 勾选 Include covergroups options； d. 点 OK，报告写入文件 fcover_report.txt。

GUI 中的操作会在 Transcript 中回显为如下命令：

coverage report -detail -cvg -comments -option
-file fcover_report.txt -r /

报告会自动在 Questa SIM Notepad 中打开：

fcover_report.txt
COVERGROUP COVERAGE:
Covergroup    Metric    Goal    Status
TYPE /top/dut/sm_transitions_cvg 100.0% 100 Covered
covered/total bins: 2 2
missing/total bins: 0 2
% Hit: 100.0% 100
type_option.weight=1
type_option.goal=100
type_option.comment=
type_option.strobe=0
type_option.merge_instances=auto(0)
Coverpoint sm_transitions_cvg::int_state 100.0% 100 Covered
covered/total bins: 2 2
missing/total bins: 0 2
% Hit: 100.0% 100
type_option.weight=1
type_option.goal=100

2. 此外，还可以用 Tools > Coverage Report 菜单生成文本（textual）、HTML 和排除项（exclusion）覆盖率报告。

本章收尾

选择 File > Quit 关闭 QuestaSim，本章结束。

自测

自测

1. 本例中，不加断言时 Verilog 版设计要到 267400 ns 才报错；加上 PSL 断言后，断言在 3100 ns 就抓住了 assert_check_refresh 失败。请问是哪条 PSL 属性被抓到违反？违反的具体表现是什么？
2. PSL/SVA 里的 |-> 和 |=> 有什么区别？abort fell(reset_n) 子句的作用是什么？
3. 断言失败设为 Break 后，为什么仿真停下时还必须再敲一条 run 0 才能看到断言消息？
4. cover 指令（cover directive）和 covergroup 各自擅长什么？原文建议如何组合使用两者？
5. up_cvg 中 option.auto_bin_max = 256 是为什么？bins illegal = default; 创建的 bin 应当呈现怎样的状态才算正常？