SVA中关于采样事件的一些事儿

并行断言的执行是基于时钟的，在构建序列逻辑属性时需要注意断言执行时其中各个信号的状态，并不是采样事件可以放在SVA的任何地方都可以，往往采样事件使用不正确，检查结果可能会大相径庭。下面我们通过几个示例了解下断言中采样事件使用上的一些问题。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
    sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;
    #3 sig0 = 1'b1;sig1 = 1'b1;
    #2 sig2 = 1'b1;sig1 = 1'b0;sig0 = 1‘b0;
    #4 $stop;
end

property pr;
    @(posedge clk) （sig0 & sig1） |-> ##1 sig2;
endproperty // pr

ap : assert property(pr) $display("@%0t | p : PASSED!",$time);
     else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】

虽然在3ns时sig0、sig1和clk同时变化，但是sig0和sig1在5ns时才被采样到为1，这是因为在每个时钟周期中所有的语句都是按照一定的事件队列执行的，在3ns时时钟采样sig0和sig1，采样的是3ns时刻时间槽（time-slot）中prepone区域中sig1和sig2的值，而此时这两个值还保持上一个时间槽结束时最后的值，即全0.为此我们将时钟跳边沿（此处以上升沿为例）的时间槽展开，其执行采样过程如下图所示：

在SystemVerilog中任何语句的执行都是按照一定的事件顺序处理进行的，断言的处理也是这样的。图中sig1和sig2的采样值来自于prepone区，即来自于上一个时间槽最后确定的sig1和sig2的值。属性中表达式的析构计算发生在时间槽的Observed区，断言后将根据成功还是失败决定执行ap中的成功部分还是失败部分。

并行断言是基于采样事件的，那么就会有一个问题，在SVA三段式的描述中，clocking_event（posedge clk）应该放在assert property、property和sequence中的哪一部分呢？下面我们将通过示例来了解一下。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
    sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;
#2 sig0 = 1'b1;
#2 sig0 = 1'b0;sig1 = 1'b1;
#2 sig2 = 1'b1;sig1 = 1'b0;
    #4 $stop;
end
// sequence s1
sequence s1;
    @(posedge clk) sig1 ##1 sig2;
endsequence // s1
// sequence s2
sequence s2;
    sig1 ##1 sig2;
endsequence // s2
// property 
property p1;
    @(posedge clk) sig0 |->##1 s1;
endproperty // p1
property p2;
    @(posedge clk) sig0 |-> ##1 s2;
endproperty // p2
property p3;
    sig0 |->##1 s1;
endproperty // p3
property p4;
    sig0 |->##1 s2;
endproperty // p4
a1 : assert property(@(posedge clk)p1) $display("@%0t | p1 : PASSED!",$time);
     else $display("@%0t | p1 : FAILED!",$time);
a2 : assert property(@(posedge clk)p2) $display("@%0t | p2 : PASSED!",$time);
     else $display("@%0t | p2 : FAILED!",$time);
a3 : assert property(@(posedge clk)p3) $display("@%0t | p3 : PASSED!",$time);
     else $display("@%0t | p3 : FAILED!",$time);
a4 : assert property(@(posedge clk)p4) $display("@%0t | p4 : PASSED!",$time);
     else $display("@%0t | p4 : FAILED!",$time);
a5 : assert property(p1) $display("@%0t | p5 : PASSED!",$time);
     else $display("@%0t | p5 : FAILED!",$time);
a6 : assert property(p2) $display("@%0t | p6 : PASSED!",$time);
     else $display("@%0t | p6 : FAILED!",$time);
// illegal // a7 : assert property(p3) $display("@%0t | p7 : PASSED!",$time);
//            else $display("@%0t | p7 : FAILED!",$time);
// illegal // a8 : assert property(p4) $display("@%0t | p8 : PASSED!",$time);
//            else $display("@%0t | p8 : FAILED!",$time);
// illegal // a9 : assert property(sig0 |->##1 s1) $display("@%0t | p9 : PASSED!",$time);
//            else $display("@%0t | p9 : FAILED!",$time);
a10 : assert property(@(posedge clk) sig0 |->##1 s1) $display("@%0t | p10 : PASSED!",$time);
     else $display("@%0t | p10 : FAILED!",$time);
a11 : assert property(s1) $display("@%0t | p11 : PASSED!",$time);
     else $display("@%0t | p11 : FAILED!",$time);
// illegal // a12 : assert property(sig0 |->##1 s2) $display("@%0t | p12 : PASSED!",$time);
//            else $display("@%0t | p12 : FAILED!",$time);
a13 : assert property(@(posedge clk)sig0 |->##1 s2) $display("@%0t | p13 : PASSED!",$time);
     else $display("@%0t | p13 : FAILED!",$time);
endmodule // top_tb

【仿真结果】

通过仿真我们可以得到采样事件与断言中各种结构元素之间的关系如下表：

断言名	assert是否使用clocking_event	property是否使用clocking_event	sequence是否使用clocking_event	合法性
a1	√	√	√	legal
a2	√	√	x	legal
a3	√	x	√	legal
a4	√	x	x	legal
a5	x	√	√	legal
a6	x	√	x	legal
a7	x	x	√	illegal
a8	x	x	x	illegal
a9	x	-	√	illegal
a10	√	-	√	legal
a11	x	-	√	legal
a12	x	-	x	illegal
a13	√	-	x	legal

a8和a12错误是因为在断言的各个基本构造环节均没有clock_event，这在并行断言中是不允许的，因为对于断言中使用的各种信号如果没有clock_event是无法被采样到从而也无法实现对应的检查。a7和a9的情况类似，都属于下图这种情况。

由上图和仿真结果可以分析出，当仅sequence中有clock_event，如果在property和assert property调用该sequence时，property和assert property中的表达式与sequence有蕴含关系的表达式因为不能从sequence中获得clocking_event，编译是不通过的。由此可见clocking_event在断言的结构中传递或者说继承的关系是：当sequence在property或者assert property中与其他表达式之间存在蕴含关系，sequence中的clocking_event不能被property或者assert property中位于蕴含操作符另一侧的表达式继承使用，即蕴含操作符对于其左右两侧的序列表达式使用的采样时钟事件起到了分割的作用，其右侧的采样时钟和时间不能被左侧的序列或者表达式继承使用，但是右侧的可以被其左侧的继承使用。但是property或者assert property中的采样事件可以被sequence使用。但是有一种情况需要注意，那就是当被调用的sequence在property或者assert property与其他表达式没有蕴含关系时，仿真会正常进行，如下例所示。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig1,sig2;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
sig1 = 1'b1;sig2 = 1'b1;
#2 sig1 = 1'b0;
#2 sig2 = 1'b0;sig1 = 1'b1;
#4 sig1 = 1'b0;$stop;
end
sequence s;
    @(posedge clk) sig1 ##1 sig2;
endsequence // s
property p;
    not s;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
  else $display("@%0t | p : FAILED!",$time);
endmodule

【仿真结果】

因为s被p调用后与p中其他表达式之间不存在蕴含关系，所以此时仅仅sequence中有clocking_event是允许的。对于断言各个基本组成环节中都没有提供clocking_event的情况，在SVA中可以使用默认时钟快结构，从而各组成环节中都可以不具体指明clocking_event，都会按照默认时钟结构中指定的时钟进行运算检查。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
Sig0 = 1’b0;sig1 = 1’b0;sig2 = 1’b0;
#2 sig0 = 1’b1;
#2 sig0 = 1’b0;sig1 = 1’b1;
#2 sig2 = 1’b1;sig1 = 1’b0;
#4 $stop;
end
// default clocking
default clocking cb
    @(posedge clk);
endclocking // cb
// sequence
sequence s;
    sig1 ##1 sig2;
endsequence // s
property p;
    sig0 |-> ##1 s;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
  else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中没有明确在各基本组成环节（sequence、property、assert property）使用clocking_event，但是在整个模块中使用了default clocking时钟块，所以各基本组成环节使用的实际上是default clocking中指定的时钟。即在当前作用域内通过使用default clocking声明时钟块，后续没有明确clocking_event的断言结构将默认使用该时钟块定义的时钟作为其采样时钟，但是需要注意在同一个module中只能定义一个default clocking块。除此之外还可以将sequence或者property声明定义于clocking块中，此时sequence和property中的各种时序关系将都是基于clocking指定的clocking_event。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk,clk1;
logic sig0,sig1,sig2,sig3,sig4,sig5;

initial begin
    clk = 1'b0;
    clk1 = 1'b0;
    fork
        forever #1 clk = ~clk;
        forever #2 clk1 = ~clk1;
    join
end

initial begin
    sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;
    sig3 = 1'b0;sig4 = 1'b0;sig5 = 1'b0;
    #2 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b1;sig3 = 1'b1;
    #2 sig2 = 1'b1;sig1 = 1'b0;
    #2 sig3 = 1'b0;sig4 = 1'b1;
    #2 sig2 = 1'b0;
    #2 sig5 = 1'b1;sig4 = 1'b0;
    #4 sig5 = 1'b0;$stop;
end

default clocking cb0
    @(posedge clk1);
endclocking // cb0
// sequence
sequence s1;
    sig1 ##2 sig2;
endsequence // s1
sequence s2;
    sig4 ##1 sig5;
endsequence // s2

clocking cb @(posedge clk);
    property p1;
        sig0 |->##1 s1;
    endproperty // p1
endclocking // cb

property p2;
    sig3 |->##1 s2;
endproperty // p2
// assertion
a1 : assert property(cb.p1) $display("@%0t | a1 : PASSED!",$time);
     else $display("@%0t | a1 : FAILED!",$time);
a2 : assert property(@(posedge clk) cb.p1) $display("@%0t | a2 : PASSED!",$time);
     else $display("@%0t | a2 : FAILED!",$time);
a3 : assert property(p2) $display("@%0t | a3 : PASSED!",$time);
     else $display("@%0t | a3 : FAILED!",$time);
endmodule // top_tb

【仿真结果】

从仿真结果可以看出，虽然a2中断言时使用了clk1，但是因为调用其的property定义于clocking cb中，其使用的时钟变为了clk而不是clk1，由此可见，对于定义于clocking cb中的assert property或者property，其采样的时钟不受clocking cb之外的时钟影响，即不管外部的sequence定义中是否存在采样事件，此时对于sequence中序列表达式的检查都是基于调用其的clocking cb的。同样的，default clocking定义的时钟也不会对其他clocking cb中定义的assert property或者property产生影响。

在基于时钟的电路中，电路运行过程中时钟是在不停的翻转，那么基于时钟的并行断言是如何伴随着时钟在时序电路中进行检查的呢？请看下例。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
    sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;
    #2 sig0 = 1'b1;
    #2 sig1 = 1'b1;
    #2 sig2 = 1'b1;
    #6 sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;
    #2 sig0 = 1'b1;
    #2 sig1 = 1'b1;
    #2 sig2 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;
    #4 $stop;
end
// de***t clocking cb1
default clocking cb1
    @(posedge clk);
endclocking // cb1
// sequence s1
sequence s1;
    sig1 ##1 sig2;
endsequence // s1
property p1;
    sig0 |-> ##1 s1;
endproperty // p1
// assertion
a : assert property(p1) $display("@%0t | p1 : PASSED!",$time);
   else $display("@%0t | p1 : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中，chk1中，sig0为高后一个时钟周期sig1为高，而此时时钟采样到sig0为高，触发chk2.再过一个时钟周期sig2为高，chk1断言成功，此时sig1仍为高，触发chk3，再过一个时钟周期sig2仍为高，此时sig3为高，chk2断言成功，与此同时sig1仍为高，触发chk4，再过一个时钟周期sig2为高，sig1仍为高触发chk5，再经过一个时钟周期，sig3为低，chk4断言失败，sig2此时也为低，chk5断言失败。由此可见，并行断言触发后并不会阻塞其他断言的进行，也就是说多个并行断言之间是相互独立的，但是这样不停的检查方式会严重影响仿真器的性能，为此SVA提供了一种内嵌的边沿函数（$rose/$fell等），可以有效的避免上述采样电平导致的不停的触发断言检查的情况的出现。