valid ready 握手验证：VALID 保持、背压时序的 SVA 断言与反例

更新时间：2026-09-25。本文是「集成电路大类 · 芯片设计 · 数字验证」序列的一篇长尾专题。SVA 断言实战给过一条 valid 稳定断言的雏形，这一篇把 VALID/READY（AXI-Stream 风格）这一个微协议讲透：契约、断言、反例、覆盖四件事一次做齐。总线级的 AXI/AHB 通道顺序、outstanding、ID 排序不在本篇范围，见 AMBA AXI UVM 验证环境与协议总线验证实战。

本文要回答的问题

VALID/READY 握手的精确契约是什么？谁等谁、谁可以变、谁不能撤？
怎么写一组并发 SVA，把「VALID 保持、数据稳定、握手当拍采样」钉死？
该用哪些反例和覆盖点，证明 stall、背压、0/1/N 拍延迟都真正被测到？

一、微协议的四条契约

VALID 由发送方驱动，表示本拍 data（以及 keep、last 等载荷）有效；READY 由接收方驱动，表示本拍能接收。二者在时钟上升沿同拍都为高即完成一次传输（transfer）。契约只有四条，但每一条都对应真实的 RTL bug：

编号	契约	违反后的典型故障
C1	VALID 一旦拉高，在握手完成前不得撤销	接收方按 VALID 推进，数据被吞或状态机跑飞
C2	等待期间整拍载荷（data/keep/last…）必须保持稳定	握手当拍采样到被偷换的新数据
C3	READY 没有稳定性义务：可提前拉、可滞后、可组合依赖 VALID	误以为 READY 也要保持，会把合法激励误报为违规
C4	只在 VALID&&READY 同高的那一拍发生一次传输；VALID 握手后当拍即可撤	用 `$rose(valid)` 当使能，背靠背第二拍被丢

注意 C1/C2 只约束握手前：握手完成的下一拍，VALID 撤销、数据换帧都是合法的。C4 的「奇偶反例」尤其常见——握手后 VALID 继续保持高就是连续两拍传输，任何只在 VALID 上升沿推进一次的设计，都会在偶数拍丢数据、奇数拍正常，症状随帧长奇偶交替出现。

还要澄清两个边界。其一，READY 允许由 VALID 组合决定（接收方看见 VALID 当拍才算出 READY），协议不要求两条信号之间有先后顺序，只要求双方都在同一个上升沿采样；真正被禁止的是反过来——VALID 去等 READY 再决定本拍数据，那等价于 VALID 依赖当拍 READY 的组合环风险，属于设计问题而非协议自由。其二，复位释放后 VALID 的第一次拉高同样受 C1/C2 约束，不要给首拍开豁免口子，许多上电丢包的 bug 就藏在「第一次传输不算数」的假设里。

下图是一段合法时序：传输 A 经历一拍 stall（VALID 先到、READY 滞后），传输 B 是 READY 提前等住、VALID 当拍即握手的零延迟情形，最后两拍 VALID 保持为高构成背靠背传输。

valid ready 握手验证：VALID 保持、背压时序的 SVA 断言与反例示意图（第 3 张）

读图抓三个采样点：第 3 拍两个信号同高，采样到的是稳定的 A；第 7 拍 READY 先于 VALID，零等待完成 B；第 7、8 拍 VALID 没有掉下去，于是连续发生两次传输——数据通路必须在每个握手沿都推进，而不是每个 VALID 上升沿推进一次。

二、并发断言：把契约钉在时钟沿

断言放进 interface/monitor 的 clocking block 里，复位期一律 disable iff (!rst_n)，避免 X 值刷假错。下面这组断言与四条契约一一对应：

systemverilog

// C1：VALID 拉高后没握手，则下一拍 VALID 必须还在（逐拍归纳，自动覆盖任意 stall 长度）
property p_valid_held;
  @(posedge clk) disable iff (!rst_n)
    (valid && !ready) |=> valid;
endproperty
a_valid_held: assert property(p_valid_held)
  else $error("[HS] VALID dropped before READY at %0t", $time);

// C2：等待期间载荷稳定。data 扩成 {data, keep, last, id} 即覆盖整拍载荷
property p_payload_stable;
  @(posedge clk) disable iff (!rst_n)
    (valid && !ready) |=> valid && $stable({data, keep, last});
endproperty
a_payload_stable: assert property(p_payload_stable)
  else $error("[HS] payload changed while waiting at %0t", $time);

// 另一种一次性写法：VALID 拉起后一直撑到 READY 出现（语义等价，报错点更靠前）
property p_valid_until_ready;
  @(posedge clk) disable iff (!rst_n)
    $rose(valid) |=> (valid [*1:$]) ##0 ready;
endproperty

// C4：传输只在握手当拍计数；握手当拍 data 不得为 X
property p_transfer_known;
  @(posedge clk) disable iff (!rst_n)
    (valid && ready) |-> !$isunknown({data, keep, last});
endproperty
a_transfer_known: assert property(p_transfer_known)
  else $error("[HS] X sampled at handshake at %0t", $time);

两点写法上的取舍。第一，C1 用「本拍没握手则下一拍 VALID 还在」的逐拍形式，比 throughout 写法更容易被形式工具接受，且任意 stall 长度都被同一条性质覆盖。第二，C2 从 $rose(valid) 的下一拍开始检查 $stable：VALID 拉起当拍数据本来就要从空闲值切到 A，这一拍比较 $stable 必然误报。READY 一侧不写任何稳定性断言——这是 C3 的推论，READY 随 VALID 组合产生完全合法。

三、反例波形：四类违例长什么样

下图故意画了三种坏时序和一个合法但易误判的对照，每一处都应被上面的断言在当拍抓住：

valid ready 握手验证：VALID 保持、背压时序的 SVA 断言与反例示意图（第 4 张）

对照上图逐一说明：

VALID 提前撤销（反例 1，违 C1）：第 1 拍 VALID 高、READY 没到，第 2 拍 VALID 掉了。p_valid_held 在第 2 沿立即报错。若 DUT 内部恰好也用 VALID 做读使能，这次传输会被静默吞掉。
等待中换数据（反例 2，违 C2）：VALID 一直撑着，但 data 从 A2 变成 A2*，第 5 拍握手时接收方采到的是 A2*。p_payload_stable 在第 4 沿报错，比 scoreboard 在几万拍后发现数据错位快得多。
奇偶反例（违 C4）：波形上完全合法，但 DUT 若把推进使能写成 $rose(valid) && ready，背靠背传输（第一节图第 7、8 拍）的第二拍 VALID 没有上升沿，数据 C 被丢，帧长为偶数时出错、奇数时正常。这类「断言全绿、数据奇偶性出错」要靠 monitor 统计握手次数与实际接收事务数一致来抓。
合法对照：READY 在第 7 拍先于 VALID 拉高，第 8 拍当拍握手。任何在这里报错的检查器都是误把 READY 当成了需要稳定的信号。

反例的用法不是只在定向用例里跑一遍给评审看，而是要确认「断言确实在那一拍开火」：把每条坏波形单独灌进 DUT，检查器必须精确报在违例沿（第 2 沿、第 4 沿），既不能晚一拍，也不能一个坏波形触发三、四条断言。报错点和报错数量本身也是检查器质量的一部分——一条 throughout 写法的性质若在整个 stall 期间每拍重复报错，日志会被同一根因刷屏，真正的第二条错误反而被淹没。

四、覆盖：READY 延迟 0/1/N 与连续背压

断言全绿的头号骗局是前提从未发生（vacuous pass），握手检查器必须配覆盖点，确认各类时序真的发生过：

systemverilog

// READY 延迟 0：VALID 拉起当拍即握手
c_r2r0: cover property (@(posedge clk) disable iff (!rst_n)
           $rose(valid) && ready);

// READY 延迟 1：恰好 stall 一拍
c_r2r1: cover property (@(posedge clk) disable iff (!rst_n)
           $rose(valid) ##1 (valid && ready));

// READY 延迟 N：连续 stall 两拍及以上
c_r2rN: cover property (@(posedge clk) disable iff (!rst_n)
           $rose(valid) ##1 (valid && !ready)[*2:$] ##1 (valid && ready));

// 连续背压：VALID 撑住、READY 连拒四拍后才放行
c_backpressure: cover property (@(posedge clk) disable iff (!rst_n)
           (valid && !ready)[*4] ##1 (valid && ready));

// 背靠背传输：握手连续发生（专打奇偶反例）
c_back2back: cover property (@(posedge clk) disable iff (!rst_n)
           (valid && ready)[*2]);

覆盖点	防的漏测
延迟 0 / 1 / N	激励只测了无背压或固定一拍 stall，长 stall 路径（计数器、FIFO 满）从未走到
连续背压	READY 连拒期间的稳定性、满标志、水位翻转没被验证
背靠背	C4 奇偶 bug：只在 `$rose(valid)` 推进的设计在此必现

回归收尾时同时看断言失败数和这些 cover 的命中数：全绿但 c_r2rN、c_back2back 为 0，说明激励空间没有打开，应在受约束随机验证的 ready 激励里加大背压权重与突发长度，而不是签收。

五、落地清单

[ ] C1–C4 四条契约各有断言，复位期 disable，载荷按整拍打包比较；
[ ] READY 一侧不写稳定性断言，READY 早于 VALID 的场景作为合法对照跑过；
[ ] 反例四件套（撤 VALID、换数据、奇偶丢拍、合法对照）在定向用例里全部复现；
[ ] 覆盖含 READY 延迟 0/1/N、连续背压、背靠背，命中数进签收标准；
[ ] 断言只依赖接口信号，不引用 DUT 内部实现，RTL 重构后可直接复用；
[ ] monitor 以握手沿计数传输，握手次数与接收事务数对账。

总结

valid ready 握手验证的核心是四条契约——VALID 握手前不得撤销、等待中载荷稳定、READY 可随时提前或滞后、传输只在双高当拍发生一次：用逐拍归纳的并发 SVA 检查保持与稳定、用 $isunknown 守住握手采样点，用「VALID 提前撤销、等待中换数据、背靠背奇偶丢拍、READY 提前合法对照」四类反例验证检查器本身，再用 READY 延迟 0/1/N、连续背压和背靠背三组 cover 防止 vacuous pass；断言失败数与覆盖命中数同时达标，才算把这个只有两根信号线的微协议真正测穿。

入门

进阶

专家

valid ready 握手验证：VALID 保持、背压时序的 SVA 断言与反例 ​

本文要回答的问题 ​

一、微协议的四条契约 ​

二、并发断言：把契约钉在时钟沿 ​

三、反例波形：四类违例长什么样 ​

四、覆盖：READY 延迟 0/1/N 与连续背压 ​

五、落地清单 ​

总结 ​