SVA 多时钟序列与局部变量：跨时钟域断言和事务数据携带
更新时间：2026-09-25。本文是「集成电路大类 · 数字验证」实操序列里 SVA 的进阶篇。基础语法（
sequence/property、|->/|=>、重复算子、空真断言）在 SVA 断言实战 里讲过，不改 RTL 注入断言的 bind 工程做法在 SVA bind 断言绑定与断言覆盖率方法 里。这一篇只解决两个单时钟 SVA 处理不了的问题：一条序列跨两个时钟域怎么写，以及怎么让一次匹配把地址、数据这类事务信息一路携带到结尾去比对。CDC 工具报告本身怎么分流签核，见 CDC/RDC 违例报告分级与签核。
本文要回答的问题
- 一条 sequence 前后挂在不同时钟上，
##1还是「延迟一拍」吗？跨时钟域能直接写##2、##[1:3]吗？ - 为什么多时钟序列里经常出现一个孤零零的
1'b1，它在同步什么？ - 子序列在另一个时钟域结束，消费端该用
.ended还是.matched？ - 局部变量在哪里声明、何时赋值，怎样做到「源域捕获地址，目的域比对数据」？
- 多时钟加局部变量的 property，编译器最常拒掉的写法有哪些？
一、单时钟断言为什么盯不住 CDC
SVA 断言实战 里的例子全部隐含一个前提：整条 property 只在一个时钟沿采样。真实芯片里大量接口不是这样。异步 FIFO 的写侧是 wr_clk、读侧是 rd_clk；跨时钟域（CDC，Clock Domain Crossing）握手里，请求在 clkA 域发起，经过两级同步器后在 clkB 域被看到，应答再同步回来。两个时钟频率不同、相位无关，不存在「共同的下一拍」。
硬用单时钟写会犯两类错。一是用快时钟去采样慢域信号，$rose 可能在一个慢域脉冲里报好几次，也可能因亚稳态窗口采到 X；二是把「同步器需要两到三个周期」写成固定 ##2，可两个异步时钟之间的相位关系每拍都在变，延迟是个区间，不存在确定拍数。
下图是一个典型电平握手 CDC：源域把请求电平翻转（toggle）并保持数据，经两级同步器进入目的域，目的域检测到边沿后采样数据，再把应答同步回去。断言要表达的契约也分布在两个域：源域管「应答回来前数据不许变」，跨域段管「目的域最终看到的必须等于源域发出的」。
为什么用 toggle（翻转电平）而不是单拍脉冲？脉冲跨域最怕目的域时钟太慢采不到——源域 200MHz 发出一个 5ns 宽的脉冲，目的域如果只有 20MHz，采样沿之间隔着 50ns，大概率整拍漏掉。电平翻转则不存在这个问题：信号一直挂在那里，目的域迟早采到，靠边沿（这一次是 0→1，下一次是 1→0）区分新旧事务。这也是跨域断言里几乎只检查电平语义、不检查固定宽度脉冲的原因。
这张图也框定了本篇的分工：SVA 不替代 CDC 结构检查（同步器有没有被综合器保留、有没有漏接，归 CDC 工具，见 CDC/RDC 违例报告分级与签核），断言检查的是功能契约——电平保持、数据稳定、跨域后内容一致。两类工具会报出不同性质的问题：CDC 工具报「这条路径没做同步」，断言报「同步是做了，但目的域收到的数据和源域对不上」。
单时钟断言和多时钟断言在思维方式上的差别，可以先用一张表对照：
| 维度 | 单时钟序列 | 多时钟序列 |
|---|---|---|
| 时间基准 | 始终是同一个沿 | 从左向右流动，遇到新时钟即切换 |
##1 含义 | 固定一个时钟周期 | 对齐到新时钟的下一个沿，宽度不固定 |
| 跨域延迟 | 任意 ##N、##[a:b] | 切换处只能 ##1，落地后再计数 |
| 适合的接口 | 模块内协议、同域总线 | 异步 FIFO、CDC 握手、多时钟 SoC 接口 |
二、多时钟序列：时钟流与 ##1 的跨时钟语义
SystemVerilog 允许在一个 sequence 里写多个时钟事件，时钟从左向右「流动」：没有新时钟的元素沿用最近的时钟。
sequence s_two_clocks;
@(posedge clkA) a ##1 @(posedge clkB) b;
endsequence这句的语义必须重新理解：a 在 clkA 沿采样成立后，##1 不再是「clkA 的下一拍」，而是「切换后时钟 clkB 的第一个严格在后的时钟沿」，然后在那个沿看 b。也就是说，跨时钟的 ##1 是一个对齐操作，对齐到新时钟，而不是一次固定宽度的延迟。下图把同一个 ##1 在单时钟和跨时钟下的落点画在一起：左半部分延迟宽度恒为一个 clkA 周期；右半部分落点取决于两个时钟的相位，可能离得很近，也可能隔着近一个 clkB 周期。
举个具体数字：clkA 是 100MHz（周期 10ns），clkB 是 60MHz（周期约 16.7ns）。a 在 100ns 的 clkA 沿成立，随后最近的 clkB 沿可能在 100.2ns，也可能在 116.9ns，取决于相位。同一个 ##1，实际间隔在 0.2ns 到 16.7ns 之间漂。断言引擎的做法是记住「我要换到 clkB 了」，然后等 clkB 的下一个事件，而不是数 10ns。
LRM（SystemVerilog 语言参考手册）对跨时钟延迟还有一条硬限制：时钟切换处只接受 ##1（以及边沿恰好对齐时的 ##0），不能直接写 ##2、##3 或 ##[1:3]。原因很直白——2 个周期是谁的周期？跨域时这个问题没有答案。##0 还有额外条件：它表示「同一时刻」，只有两个时钟沿在该拍恰好同时发生才合法，异步时钟下不要依赖，老老实实用 ##1。想在进入新时钟后数若干拍，要先「落地」再用新时钟计数，这就是下一节 1'b1 同步的用途。
三、1'b1 同步、重复等待与 ended/matched
跨时钟的标准写法是先对齐、再在新域内描述时序：
sequence s_cross_then_wait;
@(posedge clkA) a
##1 @(posedge clkB) 1'b1 // 对齐到 clkB 的第一个沿
##1 b [*2] // 此后都是 clkB 的拍：b 连续两拍
##1 c;
endsequence中间那个 1'b1 什么信号都不检查，它是一个同步占位序列（synchronizing sequence）：把匹配线程的采样时钟正式切换到 clkB。有了它，后面的 ##1、[*2] 语义才无歧义——全部按 clkB 的周期计数。工程上推荐即使语法允许直接跨域，也显式写 1'b1，读代码的人一眼能看出时钟在哪里换的。
目的域等待同步后的请求，延迟不确定，用 GOTO 式重复：1'b1 [*1:$] ##0 $rose(toggle_sync)，即「目的域一拍一拍地空转到看见同步请求的那个沿为止」。[*1:$] 的上界 $ 表示仿真全程，序列会在每个 clkB 沿试探「这一拍边沿来了没有」，来了就在当拍结束，不会多等也不会漏。若要防同步器损坏导致永远等不到（断言挂死成一个超长尝试），可以在协议层再加一条超时断言：##[1:MAX] $rose(toggle_sync)，MAX 按两个时钟的最慢频率比和同步级数留出裕量，比如 60MHz 目的域等 100MHz 源域，两级同步加相位裕量，给到十几个 clkB 周期足够。
子序列在别的时钟域结束时，涉及两个容易混的方法：
| 用法 | .ended | .matched |
|---|---|---|
| 子序列时钟与消费时钟 | 同一个时钟 | 可以不同 |
| 生效时刻 | 子序列结束的那个采样点 | 结束点被同步到消费时钟的采样点 |
| 典型场合 | 同时钟拼装复合序列 | 跨时钟域引用结果 |
sequence s_req; @(posedge clkA) $rose(req) ##1 ack; endsequence
// 在 clkB 域等 s_req 在 clkA 域的结束点，必须用 matched
sequence s_consume;
@(posedge clkB) s_req.matched ##1 done;
endsequence下图对比两者：上面一条线里子序列和消费方同在 clkA，结束当拍 .ended 即为真；下面一条线里子序列在 clkA 结束，clkB 消费方用 .matched，结束点被「搬运」对齐到随后的 clkB 沿才被看到。跨时钟误用 .ended 是高频 bug，表现为断言一次都不触发或随机漏报。
四、局部变量：让一次匹配线程带上数据
多时钟解决「什么时候」，局部变量（local variables）解决「带着什么数据」。先看单时钟最经典的需求：地址拍先到，数据拍后到，要核对的是「这一拍的数据对应之前那个地址」。
sequence s_addr_then_data;
logic [31:0] laddr; // 序列内声明局部变量
(arvalid && arready, laddr = araddr) // 握手当拍采样地址，赋值给 laddr
##1 (rvalid && rready) && (raddr === laddr); // 后续匹配中引用它
endsequence规则有四条。第一，局部变量声明在 sequence 或 property 的开头，作用域就是这一次尝试（attempt）派生出的匹配线程，两个同时在飞的事务各有各的副本，互不干扰。比如总线拍 3 发出地址 A、拍 5 发出地址 B，两次尝试各自产生线程，A 的数据在拍 6 回来时只会找到 A 那份 laddr，不会串到 B。第二，赋值写在子表达式里，用逗号连接：(布尔条件, 变量 = 值)，条件成立当拍才赋值；赋的值和右边表达式一样走采样值语义，取时钟沿之前（preponed 区域）的稳定值，不是当拍 RTL 刚更新的新值。第三，变量随线程向后流动，在之后任意深的延迟和重复中都能引用；如果序列里出现 or 分支导致线程分叉，变量按「在哪支赋的就在哪支可见」处理，两支汇合后只能引用两支都赋过值的变量。第四，计数场景直接做增减：
sequence s_burst;
int cnt;
(beat, cnt = 1)
##1 (beat, cnt = cnt + 1)[*3] // 连续 3 拍，cnt 逐拍 2、3、4
##1 (!beat && cnt == 4);
endsequence下图是局部变量随线程流动的过程：起始点把地址采样进 laddr，线程经过若干拍延迟，变量原封不动跟着走，到结束点参与比对；失败线程（起始条件没匹配上）根本不会创建这份变量。
局部变量也可以直接声明在 property 里，写法和 sequence 完全一致；区别只在于 property 还能在蕴含前件里赋值、在后件里消费，适合「某类事件触发后才开始记账」的检查。此外，一次赋值可以同时携带多个字段：(beat, laddr = addr; lid = txn_id)，一笔事务的地址、ID、长度一起捕获，后面分别比对，这在 AXI 这类带 ID 的总线断言里很常用。
局部变量可以穿过时钟边界流动——同一个线程切到新时钟后，之前捕获的数据还在。这正好是 CDC 数据一致性检查所需要的机制。需要强调的是，跨时钟时跟随线程的只有变量的值，时钟语义仍然由序列当前所在的时钟决定；不会因为变量来自 clkA，比对就按 clkA 采样。
五、完整例子：跨时钟域握手携带事务数据
回到第一节的 toggle 握手：源域 clkA 翻转 toggle 时给出 wdata，数据必须保持；目的域 clkB 从 toggle_sync 看到边沿，下一拍使能 cap_en 采样 cap_data。需要两条断言。
第一条在源域内，检查数据稳定，是普通单时钟断言：
property p_src_data_stable;
@(posedge clkA) disable iff (!rst_n)
$rose(toggle) |->
(1'b1, $stable(wdata)) [*1:$] ##1 $rose(ack_sync); // 应答回来前 wdata 不许动
endproperty
a_src_stable: assert property(p_src_data_stable)
else $error("wdata changed before ack returned");第二条是本篇的主角——多时钟加局部变量，做跨域内容一致性检查：
property p_cdc_data_match;
logic [31:0] ldata;
@(posedge clkA) disable iff (!rst_n)
($rose(toggle), ldata = wdata) // ① 源域捕获事务数据
##1 @(posedge clkB) // ② ##1 跨时钟：对齐到 clkB
(1'b1 [*1:$] ##0 $rose(toggle_sync)) // ③ 在目的域空转到看见同步边沿
##1 (cap_en) && (cap_data === ldata); // ④ 带着 ldata 比对目的域采样值
endproperty
a_cdc_match: assert property(p_cdc_data_match)
else $error("CDC data mismatch: src=%h dst=%h", ldata, cap_data);下图把这条 property 的四个步骤画成两条泳道：捕获发生在 clkA，##1 完成时钟切换，中间的空转重复对应同步器那不确定的两到三拍，最后的比对发生在 clkB，而 ldata 从第一条泳道一路带到了第二条泳道。图与代码逐段对应：图中两个域之间没有标注固定拍数，代码里对应的正是 [*1:$] 区间而非 ##2。
对照时序数字再过一遍这个例子，能验证语义确实如此：toggle 在 100ns 的 clkA 沿翻转，ldata 在那一刻采到 wdata 的采样值；##1 把线程交给 clkB，两级同步器使 toggle_sync 大约在 133.4ns 的 clkB 沿才出现 0→1；空转重复恰好在这个沿结束，下一拍 150ns 左右 cap_en 拉高，断言拿当拍的 cap_data 和跨越了约 50ns、两个时钟域的 ldata 比对。这正是 scoreboard 之外的一道贴身检查：scoreboard 可能在几百拍后才报告事务错，而这条断言在采样当拍就报错，并且报错信息里直接带着源值和目的值。
注意 cap_data === ldata 用的是 case 等等号 ===，X 和 Z 也参与比较；如果目的域采到 X（比如复位刚撤或同步器问题），断言立刻失败，而不会像普通 == 那样结果为 X、静默放过。
配套不要忘 SVA 断言实战 讲过的 cover：给 $rose(toggle) 和 cap_en 各加一条 cover property，否则源域根本没发过事务时，这条漂亮的跨域断言只会空真通过。
六、常见编译错误与采样坑
| 坑 | 典型表现 | 处理 |
|---|---|---|
| 跨时钟写固定延迟 | ##2 @(posedge clkB) 直接编译报错 | 先 ##1 @(posedge clkB) 1'b1 落地，再在新域数拍 |
| 跨时钟用区间延迟 | ##[1:3] 切换时钟处非法 | 用新时钟下的 1'b1 [*N:M] 表达 |
跨域误用 .ended | 编译报错或断言永不触发 | 子序列时钟不同一律用 .matched |
| 局部变量分支未赋值 | or 的一支没给 laddr 赋值，支后引用报编译错误 | 每支都赋值，或把引用收回到各自分支内 |
| 误把赋值当阻塞传值 | 当拍引用刚赋的值却拿到旧值 | 赋值取采样值；需要当拍新值用过程逻辑，不要用 SVA |
变量穿过 not | 局部变量不流经 not 序列 | 改写为肯定形式，或在 not 之后不引用该变量 |
| 复位期不 disable | X 被采进局部变量，后续比较全假 | property 带 disable iff (!rst_n) |
| 只 assert 不 cover | 全程无事务，全绿但零检查 | 关键起点配 cover property |
落地前再过一遍检查单：跨时钟处是否都是 ##1 加显式 1'b1；子序列跨域引用是否用了 matched；局部变量是否在每个可达分支都先赋值后引用；报错信息里是否带上局部变量值，方便直接定位是哪一笔事务跨域后变了。
这一篇在知识体系里的位置
本篇上承 SVA 断言实战（单时钟 sequence/property 基础与空真陷阱）和 SVA bind 断言绑定与断言覆盖率方法（断言工程组织），与 CDC/RDC 违例报告分级与签核 互为补充——CDC 工具查结构，SVA 多时钟序列查功能契约。断言在形式验证里同样可以直接复用，多时钟性质的证明方法见 形式验证入门。
总结
SVA 多时钟序列的本质是「时钟流」：跨时钟的 ##1 表示对齐到新时钟的下一个沿而非延迟一拍，跨域处只能用 ##1 并以显式 1'b1 同步落地，之后的重复与延迟才在新时钟域内计数，跨时钟引用子序列结果用 .matched 而不是 .ended；局部变量在 sequence/property 内声明、在匹配点以采样值赋值并随线程流动，可穿过多拍、重复乃至时钟边界，因此能写出「源域 ldata = wdata 捕获、目的域 cap_data === ldata 比对」的跨时钟域握手一致性断言；最需要盯防的是跨域写固定延迟、跨域误用 ended、局部分支未赋值和只 assert 不 cover 这四类坑。