李丽莎世界杯_2018年俄罗斯世界杯预选赛 - peacefs.com
李丽莎世界杯_2018年俄罗斯世界杯预选赛 - peacefs.com
世界杯女团决赛

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

admin

在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 【仿真结果】