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的结束点,这里需要额外注意使用ended的sequence必须要在sequence中明确采样事件,并且与property中指定的采样事件要一致。示例中s1.ended在5ns处匹配成功,成功后等待两个采样周期后s2.ended在9ns处匹配成功,此时整个属性匹配成功,可见两个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]”四次匹配中的一次有效匹配结束点一致则认为该属性断言成功,示例中在9ns和23ns处的属性断言成功点分别是“sig2[*1:4]”的第三次匹配结束点和第四次匹配的结束点。
虽然ended已经逐渐被抛弃,但是目前绝大多数的EDA工具还是支持该结构的,正如示例中展示的,一般情况下多个sequence都是以相同的起始点作为同步比较的标志,而ended结构是以sequence的结束点作为序列检查的同步点。而且在使用时一定要注意,将要使用ended的sequence中必须要指定采样事件,并且该采样事件必须与调用该sequence的属性的采样事件一致,ended中存储了一个反映在指定采样事件处序列是否匹配成功的布尔值。