可以用定义形参( formal arguments)的方式来重用一些常用的属性。属性“arb”使用了4个形参,并且根据这些形参进行检验。其中还定义了特定的时钟。SVA允许使用属性的形参来定义时钟。这样,属性可以应用在使用不同时钟的相似设计模块中。同样的,时序延迟也可以参数化,这使得属性的定义更具有普遍性。
属性首先检査有效开始。在给定的时钟上升沿,如果在信号"a”的下降沿后的2~5个时钟周期内出现信号“b”的下降沿,那么这就是一个有效开始。如果先行算子匹配,那么属性接着检查信号“c”和信号“d”的下降沿在下一个时钟周期出现,并且确保它们在4个连续的周期都保持为低。接着一个周期后,必须检测到信号“c”和信号“d”都为高,且再过一个时钟周期应该检测到信号“b”为高。
假定这是处理三个具有相似信号的不同主控设备的仲裁器的协议,可以很容易地重用前面定义的属性来检验所有3个主控设备的接口。断言a361,a362和a363定义了每个主控接口用的检验器,分别使用了各个接口对应的信号作为属性arb的参数。
module pformal;logic clk;
logic a1, a2, a3;
logic b1, b2, b3;
logic c1, c2, c3;
logic d1, d2, d3;initial $vcdpluson();initial
begin
clk=1'b0;
a1=1'b1; b1=1'b1; c1=1'b1; d1=1'b1;
a2=1'b1; b2=1'b1; c2=1'b1; d2=1'b1;
a3=1'b1; b3=1'b1; c3=1'b1; d3=1'b1;repeat(3) @(posedge clk);
a1=1'b0;
a2=1'b0;
@(posedge clk);
a1=1'b1;
a2=1'b1;
repeat(2) @(posedge clk);
b1=1'b0;
repeat(1) @(posedge clk);
c1=1'd0; d1=1'd0;
repeat(4) @(posedge clk);
c1=1'd1; d1=1'd1;
repeat(1) @(posedge clk);
b1=1'b1;
repeat(2) @(posedge clk);a1=1'b0;
a3=1'b0;
@(posedge clk);
a1=1'b1;
a3=1'b1;
repeat(2) @(posedge clk);
b3=1'b0;
repeat(1) @(posedge clk);
c3=1'd0; d1=3'd0;
repeat(3) @(posedge clk);
c3=1'd1; d1=3'd1;
repeat(1) @(posedge clk);
b3=1'b1;
repeat(2) @(posedge clk);$finish();
endproperty arb (a, b, c, d);@(posedge clk) ($fell(a) ##[2:5] $fell(b)) |->##1 ($fell(c) && $fell(d)) ##0 (!c&&!d) [*4] ##1 (c&&d) ##1 b;
endpropertya36_1: assert property(arb(a1, b1, c1, d1));
a36_2: assert property(arb(a2, b2, c2, d2));
a36_3: assert property(arb(a3, b3, c3, d3));initial forever clk = #25 ~clk;endmodule
图1-38显示了每个接口对应的断言在模拟过程中的响应。断言a361有一个有效开始,并且检验成功。断言a363有一个有效开始但是检验失败了。
成功1(a36_1)在时钟周期4,当信号“a1”的下降沿出现时,检验开始。期望在2~5个时钟周期内信号“b1”出现一个下降沿,下降沿在时钟周期7如期出现。在下一个时钟周期,信号“c1”和信号“d1”如期望的为低,并且必须保持为低4个时钟周期。它们在时钟周期8~11都为低。接着在时钟周期12,信号“c1”和“d1”如期望的为高。然后在时钟周期13,信号“b1”如期望地为高。因此检验开始于时钟周期4,成功于时钟周期13。
失败1(a36_3)在时钟周期15,当信号“a3”的下降沿出现时,检验开始。期望在2~5个时钟周期内信号“b3”出现一个下降沿,下降沿如期在时钟周期18出现。在下一个时钟周期,信号“c3”和“d3”应该为低。由于未检测到信号“d3”为低,检验失败于时钟周期19。
