问题标签 [system-verilog-assertions]

我得到一个奇怪的断言失败。尽管相等性为真，但它失败了，如错误消息中所示。我正在对u2模块的 4 个输入进行简单的求和，并确认总和等于两个输出的总和。

我收到这些错误消息：

让我们举一个带有异步复位的广告触发器的简单示例。

q 应该在时钟的下一个边沿用 d 更新，这可以用简单的蕴涵运算符断言来编写。

但是如何在断言中捕获重置行为。我试过以下几个

这两个断言都失败了，我认为是因为没有 rst 的下一个姿势？

通过但需要自由运行的时钟并在时钟的 2 个边沿之间断言（不是 rst 的内置行为）

根据我的理解，这是一个正确的直接断言，但是我在波形查看器中看不到这个通过/失败。此外，我认为我将无法为最后一种断言写封面。

How are the following two properties different?

我有一个 SV 断言，它检查如下属性

我有如下断言：

在这里，场景是，前件为真，后件在 1 到 100 个时钟周期之间进行检查。在先行之后，由于时钟门控，时钟停止了一段时间，然后时钟再次开始滴答作响。信号my_prio[rx_prio]在时钟门控之后但在 100 个时钟周期内再次置位。但我仍然得到断言失败。

无法弄清楚失败的问题。断言检查之间的时钟门控是否有问题？还是其他原因失败？谢谢。

是否可以在序列中为断言指定绝对延迟，如下所示：

这不能确定编译。但是我只是想知道当我们想要为延迟而不是时钟周期编写断言时如何处理这种情况？

例如：我想写一个断言来检查 2 个时钟之间的偏斜关系？当偏差超过 5 ps 时，如何指定要触发的断言？

SystemVerilog 中的循环语句中是否允许并发断言？

我正在尝试编写一个断言，该断言仅在信号在“clk”的上升沿转换时才会触发。我写了下面的代码来测试我的想法

上面的代码在 VCS 中返回以下输出：

为什么断言在时间 100 时触发，而“d”在时间 150 之前保持稳定？

我有一个 SV 属性如下：

我有如下断言：

在上述属性中，我有信号s_of在整个检查过程中不应断言该信号。但这里的情况是，这个信号s_of在蕴含运算符的结果过程中被断言。因此，我的要求是禁用检查，即使在后续语句中断言了信号s_of也是如此。有没有办法做到这一点？

谢谢。

|->最近出现了一个问题，通常的蕴涵运算符 ( ) 和impliesSystemVerilog 中的运算符之间有什么区别。不幸的是，我还没有找到明确的答案。但是，我收集了以下信息：

来自SystemVerilog LRM 1800-2012：

• § 16.12.7隐含和 iff 属性：

  property_expr1 implies property_expr2
  当且仅当 property_expr1 评估为 false 或 property_expr2 评估为 true 时，此形式的属性评估为 true。

• § F.3.4.3.2派生布尔运算符：

  p1 implies p2 ≡ (not p1 or p2)

• § F.3.4.3.4派生条件运算符：

  (if(b) P) ≡ (b |-> P)

但是，LRM 并没有真正指出实际差异是什么。我假设在错误的先例（成功与空洞的成功）的情况下，它们的评估不同，但我找不到任何来源或证据证明这一假设。此外，我知道implies运算符在与 OneSpin 等形式验证工具结合使用时非常常见。

谁能帮帮我？

PS：似乎在以下书中有这个问题的答案：SystemVerilog Assertions Handbook, 3rd Edition。但是仅仅为了得到这个问题的答案，155 美元对我来说有点太多了 :)

我对 Verilog 很陌生（当然对 SystemVerilog 也是如此）。我有一个 RTL 模块来测试它的功能。我试图使用断言来做到这一点，而不是应用刺激然后观察它，这样我的模块就可以被重用..

所以无论如何，我的断言如下所示：

在这种情况下，我有read_enable_pulse一个模块内部的信号，并且

我想在没有绑定的情况下从测试台级别查看它（我也不完全知道如何）。

我试图放置testbenchmodule.mymodule.read_enable_pulse一个地方read_enable_pulse来通过层次结构，但它似乎不起作用..

谁能知道该怎么做？