问题标签 [system-verilog-assertions]

待验证的模块如下... 该模块有一个输入in1和一个输出out1，在交替的时钟周期上，out1是in1的缓冲和反相值。

我尝试使用递归属性对检查器模块进行编码。

但是，在 edaplayground 运行代码会引发此错误...

RROR VCP2000 “语法错误。意外标记：nexttime[_NEXTTIME]。‘nexttime’是 SystemVerilog 关键字，不能用作标识符。

我知道这个断言可以在没有递归的情况下完成，但我想使用递归来编写它。

** 错误：(vlog-13069) cad_property.sv(5)：“case”附近：语法错误，意外情况。

没有 disable_iff ** 错误：(vlog-13069) cad_property.sv(3)：“case”附近：语法错误，意外情况，预期禁用。

在初始匹配之后，我需要检查一个序列直到模拟结束。

我想要的是类似[*$]而不是[*1000]上面的东西。我不想给出一个巨大的数字，我想永远运行它。

这是设计代码：

如何为“Out”编写断言，因为它是多时钟设计。

我已经尝试了一个，但仍然遇到一些错误。请帮助我修改此断言或编写另一个断言：

注意：通过始终阻塞和单个时钟断言，我们可以验证输出端口。但如果可能的话，我想通过多时钟断言来做到这一点，而不需要任何总是阻塞。

对于一个工具，我正在尝试正确解析 SystemVerilog 断言，并且对某些表达式的正确优先级感到困惑。SystemVerilog 标准有一个很好的表格，他们说not> until>always优先。但我不太明白这应该如何与一元运算符的交替一起工作。

例如，由于not优先级高于until，我们显然应该有：

并且由于until优先级高于always，我们显然应该有：

但是解释以下内容的正确方法是什么？

我可以想象有两种解释可能是正确的：

• not always (r1 until r2), 因为until结合得比always, 或
• (not always r1) until r2, 因为not结合得比until

看起来 NCVerilog 15.10-p001 使用了第一种解释。标准中是否有任何地方讨论我可能错过的是否正确？似乎很难将 NCVerilog 的优先规则编码成一个好的语法......

我想编写并发断言，该断言在从 UVM 测试台对 DUT 执行一些寄存器写入后开始。

这会产生跨模块引用编译错误，因为uvm_test_top是在运行时创建的，我猜断言输入是在编译时设置的。

因此，我为此找到了一些解决方法。

在全局空间中声明一些临时变量和标志变量，如下所示：

这里使用了两个全局空间变量；最好避免。

无论哪种方式，我都可以将这些变量放在顶部并在测试中通过 $root 访问它们。但是，我不喜欢使用 $root 来解决可重用性和包问题（如果我的顶级名称更改，或者编写了单独的断言模块，测试将出错）。

我想知道有没有其他更好的方法来实现这一点？这样我就可以延迟断言的执行。即使我将它延迟 1timestamp，我也会对 uvm_test_top 进行评估（听起来很疯狂..!!）。

另外，我不想使用接口信号，因为 DUT 与协议无关，它可以支持基于 `ifdefs.xml 的不同接口。（其实这也是另一种解决方法！！）

任何帮助是极大的赞赏。

我想知道什么时候在 SVA中使用->和使用？=>之间有什么区别吗

和

请让我知道..谢谢。

在我验证 DUT 的设计规范中，要求在 active_clk 信号为高电平时生成字时钟和位时钟。我在使用 SVA 方面的经验很少，所以希望有更多经验的人可以为我指出正确的方向，或者更好的是，提供解决方案。

我有以下财产：

它告诉我们，如果a被断言，则从下一个开始clk，b应该非连续两次断言，然后c在最后一次之后的任何时间断言b。

我的问题是 if在 first和 secondc之间断言怎么办。断言应该立即失败还是继续？一些参考书说它应该失败，但我对此表示怀疑。预期的行为是什么？bb

我添加了一个立即断言来测试两个寄存器在任何给定时间都没有被编程为相同的值。我在时间 0fs 失败，因为所有值都未初始化并且是“x”。

有没有办法仅在初始时完全禁用此断言？我可以使用reg !== 1'b1比较，它也比较“x”，但我想在 0fs 之后捕捉任何“x”状态。