系统verilog断言禁用条件答案

【问题标题】：system verilog assertion disable condition系统verilog断言禁用条件
【发布时间】：2015-06-22 07:50:05
【问题描述】：

我有这个断言是为了检查时钟频率：

assert property clk_freq;
int cnt;
@(posedge fast_clk, clk_1MHz) disable_iff(!enable_check)
($rose(clk_1MHz), cnt=0) |=> (!$rose(clk_1MHz),cnt++) [*0:$] ##1 $rose(clk_1MHz), cnt==fast_clk_freq;
endproperty

在 disable_check 被置位后，fast_clk 在仿真期间（而不是从开始）开始切换。问题是断言似乎忽略了disable_iff 问题：即使断言被禁用，$rose(clk_1Mhz) 事件是否“已注册”（或者我是否遗漏了其他内容？）

【问题讨论】：

标签： system-verilog system-verilog-assertions

【解决方案1】：

没有disable_iff 关键字，它是disable iff（没有下划线）。属性可以有局部变量，但不能用assert 内联定义局部变量。将属性定义和断言实例化分开。

时钟采样似乎不正确。 @(posedge fast_clk, clk_1MHz) 表示 fast_clk 上升或对 clk_1MHz 的任何更改。 clk_1MHz 是采样的数据值，所以它不应该是一个时钟。

$rose(clk_1MHz), cnt==fast_clk_freq 是非法语法，建议：$rose(clk_1MHz) ##0 cnt==fast_clk_freq

建议的属性定义和断言实例化：

property p_clk_freq;
int cnt;
@(posedge fast_clk) disable iff(!enable_check)
($rose(clk_1MHz), cnt=0) |=> (!$rose(clk_1MHz),cnt++)[*0:$] ##1 $rose(clk_1MHz) ##0 cnt==fast_clk_freq;
endproperty

a_clk_freq : assert property(p_clk_freq);

有关断言的更多信息，请参阅IEEE Std 1800-2012 的第 16 节。

【讨论】：

调试后我怀疑还有另一个问题：如果enable_check在clk_1MHz posedges之间断言，断言仍然开始“计数”，即第一个$rose得到满足即使它发生了而enable_check 很低。 这种（意外）行为是否符合标准？