极客工场

Appearance

共 4,338 字预计阅读约 14 分钟

SVA 断言 AHB 总线：HTRANS 连续性、HBURST 边界与 HREADY 下控制信号稳定 ​

更新时间：2026-09-28。在 AHB5 协议传输机制 里我们讲过 AHB 的地址相位与数据相位流水线，而 SVA 断言实践 给出了并发断言的基本语法。这一篇把两者合起来：针对 AHB master 接口写一组能直接挂在 testbench 上的 SVA AHB 断言，覆盖三类最容易被 RTL 写错、又最难靠定向用例撞出来的协议违规——HTRANS 的 NONSEQ/SEQ 连续性、HBURST 的边界约束、以及 HREADY 拉低时控制信号的稳定性。

本文要回答的问题 ​

  • HTRANS 的 IDLE/BUSY/NONSEQ/SEQ 四种编码之间，哪些跳变是协议禁止的？
  • 一个 INCR4 或 WRAP8 的 burst 中，SEQ 拍数与 HBURST 声明值对不上，断言怎么写？
  • 为什么说「burst 跨越 1KB 地址边界」是 AHB 的硬性违规，断言里怎么算这个边界？
  • HREADY 拉低插入等待态时，HTRANS/HADDR/HWRITE 必须保持不变，这条断言的前奏怎么写才不误报？
  • 断言应该绑在 interface 里还是模块里，master 侧和 slave 侧的检查有何分工？

一、先回顾要检查的对象：AHB 两相位流水线 ​

AHB 的每一笔传输分地址相位与数据相位：地址相位里 master 驱动 HTRANS、HADDR、HWRITE、HSIZE、HBURST；数据相位里数据出现在 HWDATA 或 HRDATA 上，由 HREADY 指示完成。HREADY 为低时，当前数据相位被拉长，同时下一个地址相位也被迫保持——这就是「控制信号稳定」规则的来源。

HTRANS 两位编码四种状态：IDLE（00）表示总线空闲拍，BUSY（01）表示 master 在 burst 中间插入气泡，NONSEQ（10）表示一笔新传输（或 burst 首拍）的地址与控制与前一笔无关，SEQ（11）表示延续上一个 burst 的下一拍，地址按 HSIZE 步进。HBURST 则声明 burst 类型：SINGLE、INCR、INCR4/8/16、WRAP4/8/16。

SVA 断言 AHB 总线：HTRANS 连续性、HBURST 边界与 HREADY 下控制信号稳定 示意图（第 5 张）

这张图是后面所有断言的语义底座：HREADY 同时约束数据相位的结束与地址相位的推进，所以 SVA AHB 断言的采样条件几乎都离不开 HREADY——绝大多数协议断言只应在 HREADY==1 的拍上评估，否则同一拍地址相位会被重复计数。

为什么重复计数是大问题？设想 slave 拉低 HREADY 三拍，地址相位里 HTRANS=SEQ 被原样保持了三拍。如果断言每拍都评估「SEQ 之后应跟 SEQ 或 NONSEQ」，这三拍会各触发一次，结果碰巧全对，看起来没事；但换一条「统计 burst 内 SEQ 拍数」的断言，同一个 SEQ 就被数了三次，INCR4 会被误判成 INCR6。AHB 的地址相位是被 HREADY 定界的，不理解这一点，写出来的断言要么误报要么漏报。

还有一个背景值得记住：AHB 的控制信号由当前获得总线的 master 驱动（多层总线矩阵场景下每个 layer 各自遵守同一套规则），所以本文所有断言都站在「检查 master 行为」的立场写 assert。slave 侧的检查对象换成 HREADYOUT、HRESP 与写数据的保持，前奏结构完全一样，只是主语不同。

二、断言挂载与采样框架 ​

断言写在哪里，直接决定它能不能复用。工程上的标准做法是把 SVA AHB 断言收进一个 ahb_assertions 模块，再 bind 到 AHB interface 上，DUT 一行不改。采样用 interface 里已有的 clocking block 或直接用 posedge HCLK，disable iff (!HRESETn) 保证复位期间不评估。

systemverilog
module ahb_master_assertions (
  input logic        HCLK,
  input logic        HRESETn,
  input logic        HREADY,
  input logic [1:0]  HTRANS,
  input logic [2:0]  HBURST,
  input logic [31:0] HADDR,
  input logic        HWRITE,
  input logic [2:0]  HSIZE
);
  localparam logic [1:0] IDLE   = 2'b00;
  localparam logic [1:0] BUSY   = 2'b01;
  localparam logic [1:0] NONSEQ = 2'b10;
  localparam logic [1:0] SEQ    = 2'b11;

  default clocking cb @(posedge HCLK); endclocking

一个容易踩的坑是 HTRANS 的时序归属：master 在 HREADY 低的等待态里会一直保持 HTRANS 不变，所以「上一拍 HTRANS」要用 $past(HTRANS, 1, HREADY) 这种带门控的采样——即沿着 HREADY 为高的有效拍回溯，而不是简单的 $past(HTRANS)。AHB 断言里 $past 不带门控是最常见的误报来源。

bind 的位置也有讲究。把断言模块 bind 到 interface 上，同一个 testbench 里每个 AHB 接口实例自动各得一份检查器，实例名带层级路径，报错时能直接看出是哪一个 master 口违例。有些团队图省事把断言直接写进 DUT 的 master 模块里，短期看少一个文件，长期看污染了可综合代码，还给形式验证和 lint 流程添一堆 waiver，不建议。

端口列表刻意保持最小：本文这组检查只需要 HCLK、HRESETn、HREADY 加五个控制信号。HPROT、HMASTLOCK、HWDATA 的检查可以在同一模块里追加，但信号越多，bind 时的端口匹配面越大，接口稍有裁剪（比如 AHB-Lite 没有 HRESP 的变体）就要改断言模块，所以按检查主题分组、一个模块一个职责更好维护。

信号角色断言关注点
HTRANS传输类型NONSEQ/SEQ 连续性、非法跳变
HBURSTburst 类型SEQ 拍数、WRAP 回卷、1KB 边界
HADDR地址步进值、边界跨越
HREADY握手等待态期间控制信号稳定
HWRITE/HSIZE控制等待态稳定、burst 内不变

三、HTRANS 连续性：SEQ 不能凭空出现 ​

第一类 SVA AHB 断言检查状态机层面的合法性。协议规定：SEQ 只能跟在 NONSEQ 或 SEQ 之后（同一个 burst 内），绝不能跟在 IDLE 或 BUSY 之后；BUSY 只能出现在定长 burst（INCR4/8/16、WRAP4/8/16）或未完成的 INCR 中间，不能是 burst 首拍。

systemverilog
  // SEQ 的前一个有效拍必须是 NONSEQ 或 SEQ
  property p_seq_follows;
    @(posedge HCLK) disable iff (!HRESETn)
      (HREADY && HTRANS == SEQ)
        |-> ($past(HTRANS, 1, HREADY) == NONSEQ
          || $past(HTRANS, 1, HREADY) == SEQ);
  endproperty
  a_seq_follows: assert property (p_seq_follows)
    else $error("SEQ 出现在 IDLE/BUSY 之后，burst 链断裂");

  // 定长 burst 的 SEQ 拍数必须与 HBURST 匹配
  property p_burst_len;
    int unsigned beat;
    @(posedge HCLK) disable iff (!HRESETn)
      (HREADY && HTRANS == NONSEQ && HBURST != 3'b000
                                  && HBURST != 3'b001,
       beat = (HBURST[2] ? 16 : (HBURST[1] ? 8 : 4)))
        |-> (HREADY && HTRANS == SEQ)[*(beat-1)]
            ##0 1;
  endproperty

第一条断言用带门控的 $past 沿有效拍回溯，等待态天然被跳过。第二条用局部变量在 NONSEQ 拍记下期望 beat 数（HBURST 编码 011/101/111 对应 4/8/16 拍的 WRAP，010/100/110 对应 INCR），然后要求接下来恰好出现 beat-1 个 SEQ 拍。注意写法里 SEQ 重复序列后接 ##0 1 收尾，更严格的版本还应检查第 beat 个有效拍不再是 SEQ——一个宣称 INCR4 却发出 5 个 SEQ 的 master 同样是错的。

SVA 断言 AHB 总线：HTRANS 连续性、HBURST 边界与 HREADY 下控制信号稳定 示意图（第 6 张）

这段时序是一次 INCR4 写 burst：第 0 拍 NONSEQ，第 1、2 拍 SEQ，第 3 拍 HREADY 拉低进入等待态，HTRANS 保持 SEQ 不变（这正是第五节稳定性断言要盯的场景），第 4 拍 BUSY 插在 burst 中间，第 5 拍新的 NONSEQ 开启下一笔传输。断言评估只发生在 HREADY 为高的拍沿上，第 3 拍被门控跳过。

关于 BUSY 还要多说一句。协议允许 master 在定长 burst 中间插 BUSY 拍（比如写数据还没准备好的 FIFO 源），但 BUSY 之后必须继续原来的 burst，即 BUSY 的前一个有效拍与后一个有效拍应该处在同一个 burst 链里。对应断言可以这样写：BUSY 的前一拍是 NONSEQ/SEQ/BUSY，且 BUSY 之后不允许直接落回 IDLE 然后又宣称原 burst 继续。实际项目里最常见的违规变体是「BUSY 之后 HADDR 跳了」，这会被第四节的地址步进断言顺带抓住，所以很多团队不为 BUSY 单独立法，只在步进断言里把它纳入有效拍链。

不定长 INCR（HBURST=001）是个特例：它没有声明拍数，master 可以在任何一拍用 NONSEQ 或 IDLE 收尾，也可以一直 SEQ 下去。对 INCR 不能写「拍数必须等于 N」，只检查两件事：地址按 HSIZE 步进、不越 1KB 边界。把定长 burst 的拍数断言误套到 INCR 上，是回归里另一类经典误报。

四、HBURST 边界：1KB 红线与地址步进 ​

AHB 协议有一条硬规则：任何 burst 不得跨越 1KB（0x400）地址边界，因为 AHB 从设备的地址译码粒度最小就是 1KB，越界会让一笔 burst 落到两个 slave 上。master 的 INCR 在到达边界前必须停，定长 burst 的 NONSEQ 首地址必须保证整个 burst 落在同一 1KB 区间内。

systemverilog
  // 定长 burst 首拍：末拍地址不得越过 1KB 边界
  property p_1kb_boundary;
    int unsigned bytes;
    logic [31:0] start;
    @(posedge HCLK) disable iff (!HRESETn)
      (HREADY && HTRANS == NONSEQ && HBURST[2:1] != 2'b00,
       bytes = (HBURST[2] ? 16 : (HBURST[1] ? 8 : 4)) << HSIZE,
       start = HADDR)
        |-> ((start[31:10]) == ((start + bytes - 1) >> 10));
  endproperty

  // SEQ 拍地址必须按 HSIZE 步进（WRAP 回卷单独检查）
  property p_addr_incr;
    @(posedge HCLK) disable iff (!HRESETn)
      (HREADY && HTRANS == SEQ && HBURST[0] == 1'b0)
        |-> HADDR == $past(HADDR, 1, HREADY) + (32'd1 << HSIZE);
  endproperty

第一条在 NONSEQ 拍一次算完整个 burst 的字节跨度（beat 数左移 HSIZE 位），比较首末地址的高 22 位是否一致——同一个 1KB 区间。第二条只对 INCR 类（HBURST 最低位为 0 表示非回卷）检查线性步进；WRAP 的地址在边界回卷，需要另写一条按 wrap 区间取模的检查，一般做法是断言 HADDR[低位] 与首地址的 wrap 区间内偏移一致。

SVA 断言 AHB 总线：HTRANS 连续性、HBURST 边界与 HREADY 下控制信号稳定 示意图（第 7 张）

上图把 1KB 边界检查画成区间归属问题：断言比的不是「加了多少」，而是首地址与末地址的 HADDR[31:10] 是否相等。用区间归属而不是跨度上限来写，可以同时覆盖 HSIZE 较大、beat 数较少的边角组合。

WRAP 的回卷检查值得单独展开。WRAP8、HSIZE=2（4 字节）的 burst，wrap 区间是 8×4=32 字节对齐的块：地址线性递增到块顶后绕回块首。断言思路是在 NONSEQ 拍记下区间基址 base = HADDR & ~(beat_bytes-1)，之后每个 SEQ 拍检查 HADDR == base + (($past(HADDR,1,HREADY) - base + (1<<HSIZE)) % beat_bytes)。位运算版本更简洁也更难读，工程上建议写成上面这种取模形式，配合注释，让看报告的人一眼明白期望地址怎么算出来。

地址步进断言还有一个隐藏前提：HSIZE 在整个 burst 内不允许变。协议要求一笔 burst 的所有拍用同一个 HSIZE、同一个 HWRITE、同一个 HBURST。可以给这三个信号各加一条「SEQ 拍上值与 NONSEQ 拍一致」的稳定性断言，写法与第五节的 $stable 类似，只是参考点不是上一拍而是 burst 首拍——用局部变量在 NONSEQ 拍采样，SEQ 拍上比较。

五、HREADY 拉低期间：控制信号必须冻结 ​

等待态是 AHB 断言误报和漏报的双料高发区。协议规定：当某个数据相位因 HREADY 低被延长时，下一个地址相位的所有控制信号必须保持不变，因为 slave 还在用它们。需要冻结的信号包括 HTRANS、HADDR、HWRITE、HSIZE、HBURST、HPROT。

systemverilog
  property p_ctrl_stable;
    @(posedge HCLK) disable iff (!HRESETn)
      (HREADY == 1'b0)
        |=> ($stable(HTRANS) && $stable(HADDR)  &&
             $stable(HWRITE) && $stable(HSIZE)  &&
             $stable(HBURST));
  endproperty
  a_ctrl_stable: assert property (p_ctrl_stable)
    else $error("HREADY 低期间控制信号发生变化");

前奏用 HREADY==0 叠加 |=>（隔一拍蕴涵）：本拍 HREADY 低意味着下一拍仍是同一数据相位的延续，此时控制信号必须与本拍相同。$stable 是「与上一拍相等」的简写，天然适合这种冻结检查。注意这里不要给 $stable 加 HREADY 门控——等待态恰恰是要被逐拍检查的区间，门控会把检查整段跳过。

SVA 断言 AHB 总线：HTRANS 连续性、HBURST 边界与 HREADY 下控制信号稳定 示意图（第 8 张）

时序上第 1、2 拍 HREADY 连续为低，HWRITE 与 HTRANS 高位被冻结；第 3 拍 HREADY 回升后控制信号才允许切换。p_ctrl_stable 在第 1、2 拍各自触发一次 $stable 检查，任何一拍出现毛刺或提前换值都会立刻报出精确时间点——这类 bug 靠波形人工排查往往要翻几百拍。

这条断言抓到的真实 bug 类型，比想象中丰富。最常见的是 master 内部用组合逻辑生成下一拍的 HTRANS，等待态里输入侧某个计数器变了，HTRANS 跟着抖一拍——功能上 slave 在 HREADY 低时不采样，看似无害，但协议上它就是违规，遇到对控制信号做前瞻的逻辑（比如总线矩阵的仲裁器预解码）就会出真错。另一种变体是 HREADY 由 slave 和 master 之间的桥梁合成，桥在等待态里无意转发了上游的新地址。没有断言时，这类问题往往要到系统集成、某个特定 slave 插入等待态时才暴露，定位成本极高。

写稳定性断言时还有个小决策：$stable 对比的是「上一个时钟沿」，而 AHB 控制信号本来就应在时钟沿之后保持一整拍，所以逐拍 $stable 在语义上是严格的。如果 DUT 存在合法的半拍毛刺（某些门控时钟设计），可以退而用「HREADY 回升拍与等待态首拍一致」的端点比较写法，牺牲一点灵敏度换零误报。先紧后松、按误报实况放宽，是断言调优的一般顺序。

六、工程落地：bind、cover 与常见坑 ​

断言模块写好后，用 bind 挂到 AHB interface 实例上，master 侧检查 HTRANS/HBURST/HADDR 的生成合法性，slave 侧则检查 HREADYOUT 与 HRESP 的响应时序（slave 侧断言通常用 assume 的反面——它们是被检查对象而非约束，形式验证场景才按 assume 与 cover 的形式验证分工 翻转角色）。

systemverilog
bind ahb_if ahb_master_assertions u_ahb_chk (.*);

三个收尾建议。第一，每条 assert 配一条同前奏的 cover，断言一次没失败不代表它触发过——NONSEQ 从未出现的环境里所有 burst 断言都在空转，这在 协议检查器 monitor 化 的思路里叫「检查活性」。第二，断言信息里带上 $sampled(HADDR) 等现场值，回归 triage 时不用回放波形。第三，X 传播要小心：复位刚释放时 HTRANS 可能是 X，disable iff 之外最好再加 $isunknown 守卫，避免 X 被当成匹配值静默放行。

cover 的打法可以再细一点。除了「每个前奏至少命中一次」这种活性覆盖，还应把 HBURST 的八种编码、HSIZE 的典型档位、WRAP 回卷发生时刻都做成 covergroup 或 cover property 的 bin，回归合并后看覆盖报告，能直接回答「这组断言到底有没有被充分喂过激励」。形式验证场景里这组断言可以原样复用：master 侧 assert 变成对被检模块的约束目标，slave 侧规则在 Formal 里翻成 assume，具体分工见 assert/assume/cover 的形式验证角色。

最后谈一下性能。并发断言每拍都评估前奏，信号翻转频繁的接口上成千上万次尝试是常态。本文这组断言前奏都很轻（一两个信号比较），开销可忽略；真正贵的是带长重复序列的拍数断言，p_burst_len 那种 [*(beat-1)] 写法在每个 NONSEQ 拍都会拉起一条最长 15 拍的匹配线程，高频 NONSEQ 流下线程数线性增长。仿真变慢时优先给这类断言的 consequent 加 first_match 或改用计数器状态的写法，而不是直接注释掉断言。

坑表现处理
$past 不带门控等待态后连续性断言误报$past(sig, 1, HREADY)
等待态漏查slave 拉低 HREADY 时 master 偷换地址`HREADY==0
assert 无 cover断言从未触发，假性全绿同前奏加 cover property
复位期评估复位沿报一堆假错disable iff (!HRESETn)
X 值静默X 匹配失败但不报错前置 $isunknown 守卫

还有一类常见波形误判值得单独提醒：HTRANS 在 BUSY 和 SEQ 之间的切换经常被误读成 burst 中断。BUSY 是主机主动插入的空转拍，burst 的地址计数并不前进，后续 SEQ 的地址依然按原步进连续——断言写「BUSY 后必须是 IDLE」就错了，正确约束是 BUSY 只能出现在 burst 中途、且之后必须回到 SEQ 或终止。把这条写反，回归会整夜刷误报。

这一篇在知识体系里的位置 ​

总结 ​

SVA AHB 断言的核心三件套是：HTRANS 连续性（SEQ 只能跟在 NONSEQ/SEQ 之后、SEQ 拍数匹配 HBURST）、HBURST 边界（定长 burst 首末地址同处一个 1KB 区间、INCR 按 HSIZE 步进）、HREADY 稳定性（等待态期间 HTRANS/HADDR/HWRITE/HSIZE/HBURST 用 $stable 逐拍冻结检查）——采样统一以 HREADY 为高门控、$past 带门控回溯，再配上同前奏 cover 防假性全绿，这组断言即可 bind 到任何 AHB interface 上长期服役。