SystemVerilog Assertions应用指南 Chapter1.34 ：SVA中的多时钟定义

        SVA允许序列或者属性使用多个时钟定义来采样独立的信号或者子序列。SVA会自动地同步不同信号或子序列使用的时钟域下面的代码显示了一个序列使用多个时钟的简单例子。

sequence s_multiple_clocks;
	@(posedge clk1) a ##1 @(posedge clk2) b;
endsequence

        序列 s_multiple_clocks检验在时钟“clkl”的任何上升沿,信号“a”为高,接着在时钟“clk2”的上升沿,信号“b”为高。当信号“a”在时钟“clk1”的任意给定上升沿为高时,序列开始匹配。接着“##1”延迟构造将检验时间移到时钟“clk2”的最近的。
        上升沿,检查信号“b”是否为高。当在一个序列中使用了多个时钟信号时,只允许使用“##1”延迟构造。序列 s_multiple_clocks不能被重写成下面这种形式。

sequence s_multiple_clock_illegall;
	@(posedge clk1) a ##0 @(posedge clk2) b;
endsequence
 
sequence s_multiple_clock_illegal2:
	@(posedge clk1) a ##2 @(posedge clk2) b;
endsequence

        使用“##0”会产生混淆,即在信号“a”匹配后究竟哪个时钟信号才是最近的时钟。这将引起竞争,因此不允许使用。使用#2也不允许,因为不可能同步到时钟“ck2”的最近的上升沿。相似的技术可以用来建立具有多个时钟的属性。如下面的例子所示:

property p_multiple_clocks;
	@(posedge clk1) s1 ##1 @(posedge clk2) s2;
endproperty

        它假定序列s1没有被时钟驱动,或者它的时钟定义和“clk1”样。它又假定序列s2没有被时钟驱动,或者它的时钟定义和“clk2”一样。同样的,属性可以在序列定义之间使用非交叠蕴含运算符。下面是一个简单的例子:

property p_multiple_clocks_implied;
	@(posedge clk1) s1 |=> @(posedge clk2) s2;
endproperty

        禁止在两个不同时钟驱动的序列之间使用交叠藴含运算符。因为先行算子的结束和后续算子的开始重叠,可能引起竞争的情况,这是非法的。下面的代码显示了这种非法的编码方式：

property p_multiple_clocks_implied_illegal;
	@(posedge clk1) s1 |-> @(posedge clk2) s2;
endproperty