系统验证日志中断言的可变延迟

Question

我是一个学习系统Verilog断言的新手，并从 verificationguide.com 在线找到了断言中可变延迟的代码。但是我无法理解一些事情。 有人可以详细说明以下这些给定的描述吗？

// Copy variable value to the local variable.
(1,delay=v_delay)

1. 如何复制这些数据？

// Decrements the value of the local variable and checks for the value of ‘delay’ equals ‘0’.
(1,delay=delay-1) [*0:$] ##0 delay <= 0

2. *0是什么意思？我知道 $ 用于无限检查，直到模拟结束。如果我没错的话，为什么需要 ##0，因为它只是意味着 0 延迟？

// waits for value of ‘delay’ equals to ‘0’
first_match((1,delay=delay-1) [*0:$] ##0 delay <=0)

3. first_match函数是如何工作的，它的语法是什么？

请在下面找到代码：

//-------------------------------------------------------------------------
//                      www.verificationguide.com
//-------------------------------------------------------------------------
module asertion_variable_delay;
bit clk,a,b;
int cfg_delay;
always #5 clk = ~clk; //clock generation
//generating 'a'
initial begin 
cfg_delay = 4;
a=1; b = 0;
#15 a=0; b = 1;
#10 a=1; 
#10 a=0; b = 1;
#10 a=1; b = 0;
#10;
$finish;
end
//delay sequence
sequence delay_seq(v_delay);
int delay;
(1,delay=v_delay) ##0 first_match((1,delay=delay-1) [*0:$] ##0 delay <=0);
endsequence
//calling assert property
a_1: assert property(@(posedge clk) a |-> delay_seq(cfg_delay) |-> b);
//wave dump
//initial begin 
//  $dumpfile("dump.vcd"); $dumpvars;
//end
endmodule 

Answer 1

1( 序列delay_seq有一个从属性传递的变量cfg_delay。这实际上是分配给v_delay的，而又分配给局部变量延迟。

2( *0 称为空匹配。例如 a[*0：$] |-> b 表示 a [*0] 或 [*1] 或 [*2] ..a [$]

3( 例如 ($rose(b( ## [3：4] b(有两个可能的匹配项，($rose(b( ## [3：$] b( 可以有无限数量的匹配项。若要避免由于多个匹配项而导致意外行为，或导致断言永远不会成功，因为必须测试所有先行线程才能使属性成功。first_match运算符仅匹配评估尝试中可能多个匹配项中的第一个，并导致丢弃所有后续匹配项。