全总基层组织建设网站,深圳荷坳网站建设公司,甘肃第四建设集团网站,哈密网站制作公司在序列或者属性的内部可以局部定义变量,而且可以对这种变量进行赋值。变量接着子序列放置,用逗号隔开。如果子序列匹配,那么变量赋值语句执行。每次序列被尝试匹配时,会产生变量的一个新的备份。 module cubed(enable1, a, aa, clk);input logic [7:0] a;
input logic enable1,… 在序列或者属性的内部可以局部定义变量,而且可以对这种变量进行赋值。变量接着子序列放置,用逗号隔开。如果子序列匹配,那么变量赋值语句执行。每次序列被尝试匹配时,会产生变量的一个新的备份。 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 23bz;
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 23bz;
endendmodulemodule tb;reg clk, enable1;
reg [7:0] a;
wire [23:0] aa;cubed i1 (enable1, a, aa, clk);initial $vcdpluson();initial begin
clk 1b0;
a 8bz; enable1 1b0;
repeat(2) (posedge clk);
enable1 1b1; a 8d5;
repeat(2) (posedge clk);
enable1 1b0; a 8bz;
repeat(3) (posedge clk);
enable1 1b1; a 8d6;
repeat(2) (posedge clk);
enable1 1b0; a 8bz;
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 ,lvarlvaraa)[*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处成功。
