SVA中被抛弃的ended

【说在前面的话】ended特性已经在IEEE 1800-2009中被删除,并用triggered取代。

ended用于sequence,当在特定的采样事件处sequence的结束点到达,那么ended返回布尔值真。如果只对序列的结尾比较关注,而不是很关心序列的起始点,那么ended将非常适用。ended的使用方法主要是通过给序列名字后追加关键字“ended”来实现。

【示例】
`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig1,sig2,sig3,sig4;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end
initial begin
    sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;sig4 = 1'b0;
    #2 sig1 = 1'b1;
    #2 sig1 = 1'b0;sig2 = 1'b1;
    #2 sig3 = 1'b1;sig2 = 1'b0;
    #2 sig3 = 1'b0;sig4 = 1'b1;
    #2 sig4 = 1'b0;
    #4 $stop;
end

sequence s1;
    @(posedge clk) sig1 ##1 sig2;
endsequence // s1
sequence s2;
    @(posedge clk) sig3 ##1 sig4;
endsequence // s2
// property
property p1;
    @(posedge clk) s1 |=> s2;
endproperty // p1
property p2;
    @(posedge clk) s1.ended |-> ##2 s2.ended
endproperty // p2
// assertion
a1 : assert property(p1) $display("@%0t | p1 : PASSED!",$time);
     else $display("@%0t | p1 : FAILED!",$time);
a2 : assert property(p2) $display("@%0t | p2 : PASSED!",$time);
     else $display("@%0t | p2 : FAILED!",$time);     
endmodule // top_tb
【仿真结果】


ended用于sequence是判断当前sequence的结束点,这里需要额外注意使用endedsequence必须要在sequence中明确采样事件,并且与property中指定的采样事件要一致。示例中s1.ended5ns处匹配成功,成功后等待两个采样周期后s2.ended9ns处匹配成功,此时整个属性匹配成功,可见两个sequence是以相同的结束点作为属性的最终匹配成功,而且并不关心这两个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'b1;sig2 = 1'b0;
    #2 sig1 = 1'b0;
    #4 sig0 = 1'b1;sig2 = 1'b1;
    #2 sig0 = 1'b0;sig2 = 1'b0;
    #2 $stop;
end

sequence s;
    @(posedge clk) $fell(sig1) ##2 $rose(sig2);
endsequence // s
// property
property p;
    @(posedge clk) $rose(sig0) |-> s.ended;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);    
endmodule // top_tb
【仿真结果】

示例中属性p $rose(sig0)7ns时为真,此时意味着只有序列s结束整个属性才能成功,而示例中,s.ended(即序列s的结束点匹配)在此刻匹配,即认为此时整个属性p断言成功。

【示例】

`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'b1;sig2 = 1'b0;
    #2 sig1 = 1'b0;
    #2 sig0 = 1'b1;
    #2 sig2 = 1'b1;sig0 = 1'b0;
    #2 sig2 = 1'b0;
    #2 $stop;
end

sequence s;
    @(posedge clk) $fell(sig1) ##2 $rose(sig2);
endsequence // s
// property
property p;
    @(posedge clk) $rose(sig0) |=> s.ended;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);    
endmodule // top_tb
【仿真结果】

示例中,$rose(sig0)5ns为真,下一个采样周期(7ns)序列s结束,属性p断言成功。序列s的起点(3ns)和子序列$rose(sig0)的起点(5ns)并不在同一处,所以在使用ended时需要注意使用时其关注的是序列的结束点而不是序列的起点。

另外再将ended和指定范围的重复运算符混合使用时需要注意,因为指定范围的重复运算符会存在多个匹配点,其对应的结束点也会有多个,具体结束点为哪个取决于与其他序列的关系,如下例。


【示例】
`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2,sig3;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end
initial begin
       sig0 = 1'b0;sig1 = 1'b0;
       sig2 = 1'b0;sig3 = 1'b0;
    #2 sig1 = 1'b1;
    #2 sig2 = 1'b1;sig1 = 1'b0;
    #4 sig0 = 1'b1;
    #2 sig0 = 1'b0;
    #2 sig2 = 1'b0;
    #2 sig1 = 1'b1;
    #2 sig2 = 1'b1;sig1 = 1'b0;
    #6 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig2 = 1'b0;
    #2 $stop;
end

sequence s;
    @(posedge clk) sig1 ##1 sig2[*1:4];
endsequence // s
// property
property p;
    @(posedge clk) $rose(sig0) |-> s.ended;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);    
endmodule // top_tb
【仿真结果】

示例中虽然“sig2[*1:4]”有四次匹配,但是当$rose(sig0)发生时,并不是一定要与“sig2[*1:4]”的最后一次匹配的结束点同时发生,而是与“sig2[*1:4]”四次匹配中的一次有效匹配结束点一致则认为该属性断言成功,示例中在9ns23ns处的属性断言成功点分别是“sig2[*1:4]”的第三次匹配结束点和第四次匹配的结束点。

虽然ended已经逐渐被抛弃,但是目前绝大多数的EDA工具还是支持该结构的,正如示例中展示的,一般情况下多个sequence都是以相同的起始点作为同步比较的标志,而ended结构是以sequence的结束点作为序列检查的同步点。而且在使用时一定要注意,将要使用endedsequence中必须要指定采样事件,并且该采样事件必须与调用该sequence的属性的采样事件一致,ended中存储了一个反映在指定采样事件处序列是否匹配成功的布尔值。


全部评论

相关推荐

点赞 评论 收藏
分享
评论
点赞
收藏
分享
牛客网
牛客企业服务