极客工场

Appearance

共 4,874 字预计阅读约 16 分钟

SVA CDC 同步器断言：多时钟断言、两级同步数据稳定性与 req/ack 握手检查 ​

更新时间：2026-09-28。SVA 断言实践 把单时钟断言的写法讲透了，但真正的工程 bug 大户在时钟域边界：信号从 clka 域跨进 clkb 域，中间隔着两级触发器、握手状态机或者异步 FIFO，两边采样沿没有任何相位关系。这一篇专门讲 SVA CDC 同步器断言：如何用多时钟 property 描述跨越时钟域的因果，如何给两级同步器和握手 CDC 写出能在仿真和形式验证里同时生效的检查。

本文要回答的问题 ​

  • 单时钟断言为什么一到跨时钟域就失灵，多时钟 property 的采样语义到底是什么？
  • 两级触发器同步器应该断言什么——同步后的值还是同步前的稳定窗口？
  • req/ack 四相握手 CDC 里，哪些序列违例意味着数据会被采错或丢包？
  • 异步 FIFO 的格雷码指针跨域后，断言该盯「不丢不重」还是「指针单调」？
  • 仿真里亚稳态注不进去，这些断言在形式验证里怎么发挥真正威力？

一、为什么跨时钟域断言是另一个物种 ​

单时钟断言的全部语义建立在一个前提上：所有信号在同一个采样沿上取值，「下一拍」有唯一确定的含义。CDC（Clock Domain Crossing，跨时钟域）把这个前提拆了。clka 的上升沿和 clkb 的上升沿之间没有固定的相位关系，一个信号在 clka 域里「变化后下一拍稳定」，在 clkb 域里可能正好踩在变化中间被采走——这正是亚稳态的来源，建立保持时间与亚稳态 已经从电路角度讲过这个机制。

用单时钟思维写 CDC 断言会踩三个典型坑。第一，把断言挂在错误的时钟上：@(posedge clkb) req_a |-> ##1 ack_b，前提里 req_a 是 clka 域信号，在 clkb 沿上采样它本身就是一次未经同步的跨域，断言看到的值和 DUT 里任何一级触发器看到的都对不上。第二，把 ##1 当成「隔一小段时间」：##1 永远是「下一个采样沿」，clka 的一拍在 clkb 域里可能是 0.3 拍也可能是 3 拍，取决于频率比和相位。第三，断言只查同步器输出，不查输入稳定性——两级触发器只能消化亚稳态，消化不了「数据在采样窗口内还在翻转」这个协议错误，而后者才是 CDC 功能 bug 的主力。

所以 CDC 断言的目标要重新定位：不是证明「信号跨域后值正确」（那是设计本身要保证的），而是证明三件事——跨域的控制信号经过了同步结构、被同步的数据在采样时刻前后足够稳定、握手机构的状态迁移没有漏拍。这三件事分别对应本文第三、四节和第五节的断言写法。

SVA CDC 同步器断言：多时钟断言、两级同步数据稳定性与 req/ack 握手检查 示意图（第 6 张）

上图是整篇的视角：断言挂在跨域点的两侧，clka 侧的断言负责「送出去的东西合法」，clkb 侧的断言负责「收到的东西是同步结构处理过的」，中间的亚稳态消化交给电路，不由断言证明。

二、多时钟 property：采样沿切换的语义 ​

SystemVerilog 允许在一条 property 里切换时钟，写法是在序列或表达式前直接标注时钟事件。基本形态如下：

systemverilog
property p_req_crosses;
  @(posedge clka) $rose(req_a)
  |-> @(posedge clkb) ##[1:3] $rose(req_b_sync);
endproperty
a_req_crosses: assert property (p_req_crosses)
  else $error("req_a 跨域后 req_b_sync 未在 1-3 个 clkb 内拉起");

这条断言读作：clka 上看到 req_a 上升沿之后，把后续求值的采样沿切到 clkb，在 1 到 3 个 clkb 沿之内必须观察到 req_b_sync 拉起。|-> 是重叠蕴含，前后件的「接缝」语义是多时钟断言里最绕的地方：前件在 clka 的某个沿上匹配成功，后件的第一次采样发生在严格晚于前件匹配时刻的最近一个 clkb 沿。这个「最近沿」规则保证了语义良定义，但也带来一个后果——clkb 远快于 clka 时，后件的 ##1 可能只对应前件沿之后零点几个 clka 周期，形式工具给出的反例波形里两段时钟沿交错出现，读反例时务必先看清每条波形上的采样点标记。

多时钟序列里还有几个容易写错的点。其一，局部变量跨时钟传递是合法的，@(posedge clka) ($rose(req_a), v = data_a) |-> @(posedge clkb) ##[1:3] (data_b == v) 能表达「数据原样跨域」，这条特性的深入讨论见 SVA 多时钟序列与局部变量。其二，多时钟序列不能用 ##0 拼接不同时钟的子序列，因为两个时钟的沿不可能重合，编译器会直接报错。其三，$stable、$rose 这类采样函数取的是「当前时钟事件下」的前值与现值，断言主体时钟切到 clkb 后，$stable(data_a) 描述的是 data_a 在 clkb 相邻两沿之间没变——这正是检查数据稳定性窗口所需要的语义，下文会反复用到。

SVA CDC 同步器断言：多时钟断言、两级同步数据稳定性与 req/ack 握手检查 示意图（第 7 张）

这张双时钟波形对应上面的断言：clka 周期 2ns，req_a 在 2ns 拉起；后件采样沿切到周期 3ns 的 clkb，最近的 clkb 沿在 3ns，req_b_sync 在 5ns 的沿被观察到拉起，落在 ##[1:3] 窗口内，断言通过。把两个时钟画在同一张图里，能直观看到「##1 在两个域里对应的真实时间完全不同」——这是写多时钟延迟窗口时必须先算清楚的账。

三、两级同步器：断言的主角是数据稳定性 ​

两级触发器同步器（2FF synchronizer）是最常见的单 bit 控制信号 CDC 结构：第一级触发器把异步输入采进来，允许它进入亚稳态；经过将近一个 clkb 周期的消化时间，第二级再采一次，输出送到目标域逻辑。它解决的是亚稳态传播概率，前提是输入是单 bit、且在目标域看来「变化足够稀疏」。

对 2FF 同步器，能写的断言分三层。

第一层是结构性检查，确认同步链没被后人改断：目标域逻辑只能消费第二级输出 sig_sync2，绝不允许直接碰异步输入 sig_a。这类检查用断言表达为「目标域的组合输出只依赖 sig_sync2」，实践中更常用 lint/CDC 工具做结构检查，断言作为兜底，例如确认 sig_a 没有扇出到 sync1 之外的任何 clkb 域触发器。

第二层是同步延迟的活性（liveness）检查：

systemverilog
property p_2ff_liveness;
  @(posedge clkb) disable iff (!rstb_n)
    $changed(sig_sync1) |-> ##1 (sig_sync2 == $past(sig_sync1));
endproperty

它锁定 2FF 的寄存行为本身：sync2 永远落后 sync1 一拍。这条断言看起来 trivial，价值在于它能在集成环境里抓到「同步器被综合掉」「rst 极性接反导致 sync 链恒为 0」这类集成级错误——单元级 review 很难发现，而它的失效会让整个跨域通路静默丢信号。

第三层才是真正决定功能正确性的检查：被同步的信号在源域必须保持足够长的稳定时间。如果 req_a 是一个只有半个 clka 周期的窄脉冲，而 clkb 比 clka 慢三倍，2FF 可能整个漏采这个脉冲。断言写法是约束脉冲宽度：

systemverilog
property p_pulse_wide_enough;
  @(posedge clka) $rose(req_a) |-> req_a throughout (##[0:2] 1'b1);
  // 工程口径：req_a 至少保持 1.5 个 clkb 周期，
  // 换算成 clka 拍数按最坏频率比计算
endproperty

更稳妥的工程做法是源域干脆把信号保持到收到应答为止——这就从「脉冲同步」升级成握手 CDC，进入下一节。多 bit 数据总线走 2FF 是原则性错误：各 bit 的亚稳态消化时间不同，sync2 输出可能是一个从未在源域出现过的中间组合。多 bit 数据必须配「数据稳定 + 单 bit 控制同步」结构：源域先驱动数据并保持，再把单 bit 的 data_valid 做过 2FF，目标域看到同步后的 valid 才采数据。对应的断言是稳定性窗口检查：

systemverilog
property p_data_stable_around_valid;
  @(posedge clkb) disable iff (!rstb_n)
    $rose(valid_sync2) |-> $stable(data_b_sampled)
    && $stable(data_a_hold);  // 数据在 valid 拉起前后均不变化
endproperty
SVA CDC 同步器断言：多时钟断言、两级同步数据稳定性与 req/ack 握手检查 示意图（第 8 张）

上图把「数据不经过触发器同步、靠稳定窗口保证正确」的结构画清楚了。断言 p_data_stable_around_valid 检查的是窗口右端，左端（源域何时允许改数据）要靠握手协议的 ack 来界定，单层 2FF 给不了这个界定，这也是它在多 bit 场景必须升级成握手的根本原因。

四、握手 CDC：req/ack 序列的完整检查清单 ​

四相握手（req 升起 → 目标域采数据 → ack 升回 → req 落下 → ack 落下）是多 bit 数据跨慢时钟域的标准做法。它比 2FF 多花一倍以上延迟，换来的是「数据在采样前后都被协议锁死」的确定性。对应的 SVA 检查是一份序列清单，漏任何一条都对应一类真实 bug：

systemverilog
// 1. req 必须在 ack 回来之前保持（源域视角）
a_req_hold: assert property (
  @(posedge clka) disable iff (!rsta_n)
    $rose(req_a) |-> req_a until_with $rose(ack_a_sync)
) else $error("req 未保持到 ack");

// 2. ack 只能由 req 引起，不许无中生有（源域视角）
a_no_spurious_ack: assert property (
  @(posedge clka) disable iff (!rsta_n)
    $rose(ack_a_sync) |-> req_a
) else $error("ack 在 req 未拉起时出现");

// 3. 数据从 req 拉起到 ack 返回全程稳定（源域视角）
a_data_stable: assert property (
  @(posedge clka) disable iff (!rsta_n)
    $rose(req_a) |-> $stable(data_a) throughout
      (req_a [*1:$] ##1 $rose(ack_a_sync))
) else $error("握手期间数据被改写");

// 4. 目标域确实消费了数据（活性，clkb 视角）
a_dst_consumes: assert property (
  @(posedge clkb) disable iff (!rstb_n)
    $rose(req_b_sync) |-> ##[1:4] $rose(ack_b)
) else $error("目标域收到 req 后未产生 ack");

// 5. req 落下后 ack 必须跟着落下（回到空闲，四相完整性）
a_ack_falls: assert property (
  @(posedge clka) disable iff (!rsta_n)
    $fell(req_a) |-> ##[1:$] $fell(ack_a_sync)
);

五条断言分工明确：第 1、3 条保护数据完整性，违反即「目标域采到半截数据」；第 2 条防状态机错乱，ack 凭空出现会让源域误以为上一笔交易完成而改写数据；第 4 条是活性，防死锁——req 永远等不到 ack 在仿真里表现为超时，有了这条断言能直接定位到「目标域状态机卡在哪个状态」；第 5 条保证状态机能发起下一笔交易，四相握手如果只做了两相，第二笔交易的 req 上升沿会被目标域误认为还是第一笔，造成数据重复消费。

写这份清单时有两个频率相关的细节。其一，req/ack 各自都要过 2FF 跨域，所以第 1 条里的 until_with 匹配时刻天然包含了两个同步延迟，不需要手工补 ## 余量。其二，clkb 远快于 clka 的场景里第 4 条的 ##[1:4] 窗口要按 clkb 拍数给，而整个握手完成时间按 clka 拍数可能是几十拍——写活性断言的延迟上界时，永远用「采样时钟自己的拍数」度量，再按最坏频率比反推，CDC 基础与跨域结构选型 里有一张延迟预算表可以直接套。

SVA CDC 同步器断言：多时钟断言、两级同步数据稳定性与 req/ack 握手检查 示意图（第 9 张）

这张波形把五条断言的检查点全部标在了一张图上：2ns req 升起（第 3 条开始盯数据稳定），5ns req_b_sync 到达目标域（第 4 条活性窗口开启），8ns ack_b 产生，10ns ack_a_sync 回到源域（第 1 条 until_with 匹配、第 3 条窗口关闭），随后 req 落下、ack 逐级落下（第 5 条）。任何一个环节信号提前或缺席，对应的断言编号就是定位起点。

五、异步 FIFO 与格雷码指针的断言 ​

数据通路是流式的而不是逐笔的，握手就太贵了，标准答案是异步 FIFO：写指针在写时钟域递增，读指针在读时钟域递增，两边各自把对方的指针值用格雷码 + 2FF 同步过来再算满空。完整的验证方案见 异步 FIFO CDC 验证，这里只抽出断言部分的核心——指针跨域后的性质。

格雷码的特性是相邻计数值只差一个 bit，因此指针总线整体跨域时，即使采在跳变瞬间，sync2 得到的也至多是「旧值」或「新值」，不会是第三种组合。对应的断言分两类。

第一类是指针单调性与格雷性检查（在各指针自己的时钟域内写，最容易被忽略却最有价值）：

systemverilog
// 写指针二进制形式每次只加 1（满时保持）
a_wptr_step: assert property (
  @(posedge wclk) disable iff (!wrst_n)
    (wptr_bin != $past(wptr_bin)) |->
    (wptr_bin == $past(wptr_bin) + 1'b1)
);
// 格雷码形式相邻值只差一个 bit
a_wptr_gray: assert property (
  @(posedge wclk) disable iff (!wrst_n)
    (wptr_gray != $past(wptr_gray)) |->
    $onehot(wptr_gray ^ $past(wptr_gray))
);

$onehot(a ^ b) 是「恰好一个 bit 不同」的一行写法，它把格雷码的构造前提变成了运行时可查的断言——一旦有人把指针改成带提前终止的计数器（比如包边界回卷），这条断言立刻报警，而同步过去的指针在远端产生的满空判断错乱极难从功能波形反推。

第二类是同步后指针的「旧值或新值」检查，即跨域指针不能落到跳变序列之外：

systemverilog
// 读时钟域看到的写指针，只能是「过去某个真实值」
a_synced_ptr_legal: assert property (
  @(posedge rclk) disable iff (!rrst_n)
    $changed(wptr_gray_sync2) |->
    (wptr_gray_sync2 == $past(wptr_gray_sync1))
);

满空标志的保守性是第三类：full 可以在写域「虚报」（同步延迟导致看到滞后的读指针），empty 同理，但绝不允许反向——full 漏报会让写端溢出覆盖未读数据，empty 漏报会让读端采到无效 RAM 内容。FIFO 的不丢不重最终由 scoreboard 保证，断言负责把错误定位到「指针」「标志」还是「RAM 读写使能」中的哪一环。格雷码指针 CDC 的设计细节 和 异步 FIFO 结构设计 两篇从设计侧把这里断言的每一条前提都推导过。

六、覆盖点与形式验证：让断言真正咬到亚稳态 ​

仿真有个先天性短板：寄存器模型不会真的进入亚稳态，两个异步时钟即使按无理数频率比跑，「恰好在采样窗口内跳变」的事件也未必出现，2FF 的第一级在仿真里永远表现得像理想触发器。所以 CDC 断言在仿真里的角色主要是协议检查（第四节那份清单），而亚稳态注入和穷尽性证明要交给形式验证。

形式侧的标准打法分两步。第一步，把跨域输入在 formal 环境里放开为任意值（cutpoint），让工具穷尽「任何相位、任何跳变时刻」；此时第三、四节的稳定性与握手断言如果写法正确，应该全部prove 或给出真实反例——给出反例说明设计在某种相位组合下确实会采到不稳定数据，这就是仿真几乎不可能撞到的那类 bug。第二步，对活性断言（第 4 条那种 ##[1:4]）做 bounded proof，深度按两个同步链加状态机最长路径估算。形式验证应用与 FPV 流程 讲了 cutpoint 与证明深度的通用做法，assert/assume/cover 在形式里的角色分工 则解释了为什么源域的稳定性约束在形式里要写成 assume 而不是 assert。

覆盖点（cover）在 CDC 验证里同样不能省，至少要埋这几处：req/ack 握手完整走一轮的序列 cover；full 和 empty 各自拉起的 cover；「写读同时进行且指针同步链上有跳变」的交叉 cover——它强制激励打到「同步器正在消化亚稳态的同时对方在采样」的场景，没有这个 cover，回归可能跑了一万次却从没让指针跨域和读采样撞在同一时刻。

SVA CDC 同步器断言：多时钟断言、两级同步数据稳定性与 req/ack 握手检查 示意图（第 10 张）

上图是三条通路的互补关系：结构工具确认同步器存在且未被打断，仿真断言盯协议序列，形式断言穷尽亚稳态相位。只跑其中任何一条，都有整类 bug 漏网的明确路径——CDC 报告的 triage 方法在 CDC/RDC 报告分类与处理 里，本文写的断言正是把报告里的「疑似违例」变成「仿真/形式可重现失败」的翻译层。

七、常见坑 ​

  • 把断言时钟挂错域：前提在 clka、结论想当然用了 clkb 信号却不切换时钟事件，断言采样到的就是未同步的原始信号，结果和设计行为对不上。
  • 用 ##1 当时间：跨时钟后延迟必须按「后件时钟的拍数」重算，并把最坏频率比折算进上界。
  • 给多 bit 数据总线写 $stable 窗口却忘了约束源域保持到 ack：窗口右端再稳，左端在半路被改写一样采错。
  • 活性断言上界拍脑袋：上界给小了形式工具报出假反例，给大了 bounded proof 跑不完；按「两级同步 + 状态机最长响应」逐段估算。
  • 只在仿真跑断言就签收：仿真注不进亚稳态，协议断言全绿不代表跨域安全，形式 cutpoint 证明是必经环节。
  • 忘埋 cover：断言全 vacuous pass（前提从未触发）和断言全绿在报告里长得一样，必须配前提命中的 cover 才能区分「没问题」和「没测到」。
  • 格雷码假设不检查：$onehot(gray ^ $past(gray)) 一行断言的事，漏了它，指针改型后所有下游满空断言都在检查一个错误前提。
  • reset 跨域不管：两个域的 reset 释放时刻也是一次 CDC，disable iff 只关了断言，没关掉「对端还在复位时本端发起握手」的真实风险场景，要单独写复位退出序列的检查。

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

总结 ​

SVA CDC 同步器断言的核心是把跨时钟域的因果关系翻译成多时钟 property：用 @(posedge clka) ... |-> @(posedge clkb) ... 表达采样沿切换，用「req 保持到 ack、数据全程 $stable、ack 不无中生有、四相完整回落」这份清单锁死握手 CDC，用 $onehot(gray ^ $past(gray)) 与「同步指针只能是旧值或新值」守住异步 FIFO——仿真断言抓协议违例，形式 cutpoint 穷尽亚稳态相位，两条通路都绿了，跨时钟域才算真正验完。