SVA中的multi-clock
现在的设计中经常存在不同时钟域的信号之间的交互（CDC：Clock Domain Crossing），这些信号之间的逻辑关系也相当复杂，SVA中提供了解决这种多时钟域信号之间复杂逻辑关系的检查。在SVA中允许序列或者属性使用中对其中的子序列或者信号采用不同的时钟进行采样，并且在检查时会在不同采样事件检查的序列之间自动的进行“同步处理”。本文将示例说明SVA如何在多时钟域信号之间进行检查。
【示例】
`timescale 1 ns / 1 ps
module top_tb;
logic clk0,clk1;
logic sig0,sig1;
initial begin
clk0 = 1'b0;
forever #1 clk0 = ~clk0;
end
assign clk1 = ~clk0;
// stimulus
initial begin
sig0 = 1'b0;sig1 = 1'b0;
#2 sig0 = 1'b1;#1 sig1 = 1'b1;
#1 sig0 = 1'b0;#1 sig1 = 1'b0;
#4 $stop;
end
// property
property p;
@(posedge clk0) $rose(sig0) |-> ##1 @(posedge clk1) $rose(sig1);
endproperty // p
// assertion
a : assert property(p) $info("@%0t | p : PASSED!",$time);
else $info("@%0t | p : FAILED!",$time);
endmodule // top_tb 【仿真结果】 
示例中，sig0基于采样事件clk0，sig1基于采样事件clk1。$rose(sig0)在3ns处clk0采样匹配后，仅等待了半个clk1子序列“##1 @(posedge clk1) $rose(sig1)”即在4ns处匹配，这是因为此时是距离$rose(sig0)满足要求后最近满足“@(posedgeclk1) $rose(sig1)”的时刻点，因为属性的所有子序列都匹配，所以断言此刻成功。为什么会这样呢？这是因为在多采样事件的序列中，基于第一个采样时间的序列满足要求后，紧接着其后的基于另一个采样时间的子序列采用其第一次匹配的结果作为其匹配的结果，这里的基于另一个采样事件的子序列的第一次匹配不一定是一个完整的采样周期，而是距离基于第一个采样事件后其最近的第一次匹配。同时还需要注意如果“##1”左右两侧的采样事件不同（不同频不同相），那么其两侧只能使用“##1”进行延迟，这样能够保证“##1”的右两侧子序列采用最近的匹配，当然如果试图使用其他值仿真器是不同意的。在实际使用过程中也会遇到如下几种情况：
【clk0周期小于clk1周期】
【clk0与clk1同频同相，相当于采用同一个采样事件的情况】
【clk0周期大于等于clk1周期】
上述几种采用多时钟的不同子序列的匹配情况中，会在clk0采样的子序列匹配后，基于clk1采样的子序列采用距离clk0匹配最近的一次匹配，即基于不同时钟域的子序列的匹配采用的是“最近匹配”原则。
