在系统 verilog 中使用 $past 宏来获得高信号答案

【问题标题】：usage of $past macro in system verilog for a signal to high在系统 verilog 中使用 $past 宏来获得高信号
【发布时间】：2020-09-10 06:56:51
【问题描述】：

我是系统verilog的初学者。

我想在信号的下降沿检查它在过去的“n”个周期内是否为高电平。 ##n 个循环的使用对我不起作用。

逻辑 x,y;

x & y -> ##2 $past(y) -> $fell(y);这似乎不起作用

在 x & y 的条件下，我检查的是在 'y' 的下降沿，在满足条件 x& y 后的过去 2 个周期内，信号 'y' 为高电平

【问题讨论】：

标签： system-verilog system-verilog-assertions

【解决方案1】：

您好，欢迎来到 SVA。

在我的回答中，我假设您已经定义了一个时钟并在您的“下降沿”定义中使用它

您的代码和问题描述存在一些问题。我仅列举这些以帮助解决将来的问题： - $past 不是宏而是系统函数 - 您没有使用正确的 SVA 隐含运算符。 “->”是一个阻塞事件触发器。我猜你想要的重叠蕴涵运算符是 |-> - ##2 $past(y) 实际上会插入 2 个周期的延迟，然后检查 y 的过去值是否很高。确实，您正在检查 y 在初始触发后一个周期是否为高。

我也不太确定你的触发条件是什么——如果 x 和 y 都很高，x && y 将产生一个属性线程。事实上，它不会在 y 的否定上触发。

在下面的代码中，我尝试按照我的理解将 SVA 编码为您的规范。您可以使用一个简单的函数来确保在前 n 个循环中，y 为高。随意根据需要用任何触发器替换 $fell(y)。

function bit y_high_preceding_n_cycles(int n)
 for(int i = 1; i < n; i++) begin
  // check if y wasnt high i cycles ago, just return 0
  if (!$past(y, i, , @(posedge clk))) return 0;
 end
 return 1;
endfunction

prop_label: assert property($fell(y) |-> y_high_preceding_n_cycles(n));

这将检查在检测到 $fell(y) 时，y 在前 n 个周期中是否为高。请注意，根据定义，for 循环 i==1 的迭代将是多余的（作为 $fell(y) 上的触发器，即绝对 $past(y) == 1 假设没有 Xs）。

希望这会有所帮助。

【讨论】：

谢谢你，我能得到我想要的东西。