SystemVerilog Assertions应用指南 Chapter1.37 使用局部变量的SVA

        在序列或者属性的内部可以局部定义变量,而且可以对这种变量进行赋值。变量接着子序列放置,用逗号隔开。如果子序列匹配,那么变量赋值语句执行。每次序列被尝试匹配时,会产生变量的一个新的备份。

module cubed(enable1, a, aa, clk);input logic [7:0] a;
input logic enable1, clk;
output logic [23:0] aa;reg [7:0] valid_a;
reg [23:0] temp_aa;initial begin
aa = 23'bz;
endalways@(posedge clk)
beginif(enable1)valid_a <= a;
endalways@(valid_a)
begintemp_aa <= valid_a * valid_a * valid_a;repeat(4) @(posedge clk);aa <= temp_aa;repeat(1) @(posedge clk);aa <= 23'bz;
endendmodulemodule tb;reg clk, enable1;
reg [7:0] a;
wire [23:0] aa;cubed i1  (enable1, a, aa, clk);initial $vcdpluson();initial begin
clk = 1'b0;
a = 8'bz; enable1 = 1'b0;
repeat(2) @(posedge clk);
enable1 = 1'b1; a= 8'd5;
repeat(2) @(posedge clk);
enable1 = 1'b0; a = 8'bz;
repeat(3) @(posedge clk);
enable1 = 1'b1; a= 8'd6;
repeat(2) @(posedge clk);
enable1 = 1'b0; a = 8'bz;
repeat(4) @(posedge clk);
$finish();
endinitial forever clk = #25 ~ clk;property p_local_var1;
int lvar1;@(posedge clk) ($rose(enable1), lvar1 = a) |-> ##4 (aa == (lvar1*lvar1*lvar1));
endpropertya_local_var1: assert property(p_local_var1); endmodule

        属性 p_local_var1查找信号“ enable”的上升沿。如果找到,局部变量“ lvar1”保存设计中向量“a”的值。在4个周期后,检查设计的输出向量“aa”是否与局部变量的值的立方相等。属性的后续算子等待设计满足延迟(4个时钟周期),然后将设计的实际输出和属性局部计算的值比较。图1-41显示了检验在模拟中的响应。

        标记1s显示了信号“ enable1”的上升沿被采样到的点,在这点,向量“a”的值为5,被保存在局部变量“lvar1”中。标记1e标出了输岀被釆样的点,它在输入值被保存的4个时钟周期之后。在标记1e的点,因为输出值(125)与局部变量“ Ivar1”的值的立方相等,断言成功。类似地,标记2s显示了下一个输入数据被保存的时刻,标记2e标出了输出被采样并且与局部变量“ Ivar1”的立方值比较的时间点。
        可以在SVA中保存和操作局部变量。

property p_lvar_accum;int lvar;@(posedge clk) $rose(start) |=>(enable1 ##2 enable2 ,lvar=lvar+aa)[*4]##1 (stop && (aout ==lvar));
endpropertya_lvar_accum :assert property(p_lvar_accum);

        属性 p_Ivar_accum检查下列内容:
                (1)在任意给定的时钟上升沿,如果检测到信号“ start”的上升沿,标志一个有效开始。
                (2)在一个周期后,寻找一个特定的模型或者子序列。信号“ enable1”必须被检测为高,且两个周期后,“ enable2”应该被检测为高。这个子序列必须连续重复4次。
                (3)在子序列的每次重复中,向量“a”的值在序列内部被累加。在重复结束时,局部变量保存着向量“a”累加4次的值。
                (4)在重复结束的下一个时钟周期,期望信号“stop”为高,且局部变量保存的值与输出向量“aout”的值相等。图1-42显示了检验在模拟中的响应。

        标记1s显示了当信号“start”被检测为高时所产生的一个有效开始。标记1e显示了检验的结束点。信号“ enable*”成功地重复4次并且在一个时钟周期后,信号“stop”如期望的被检测为高。局部变量保存的值与输出向量“aout”值相同,因此检验在标记1e处成功。