问题标签 [system-verilog-assertions]

我想写一个断言，它说 req 应该在下一次完成后 4 个周期变高。对我来说，重置完成已经很高了。我怎样才能在下一次完成时提出更高的要求。assert property {$rose(done) |-> ##4 req}但我不知道为什么它不起作用。有人可以帮忙吗？

我是 systemverilog 和 SVA 的新手，我正在尝试为 prbs 生成器创建一个断言，logic [6:0]在 127 个时钟周期后将任何给定的数组 ( ) 与相同的数组进行比较。问题是我发现有助于比较数组的运算符不允许并发，而允许并发的运算符仅使用位进行操作。

试图举例说明我想做的事情是这样的：

在 SystemVerilog 断言 (SVA) 中，为什么使用：

一个坏主意？是否是由于暗示的成功方面的空洞（即，何时a不正确）？

以下陈述之间的细微差别是什么

a -> b对比a ##0 b

在 SVA（SystemVerilog 断言）中？

假设我们有一个协议，它说明了以下内容。一旦主机设置req为fill，从机将通过以下方式发出 4 次传输信号rsp：

整个事务的 SVA 序列将是（假设从设备可以在idle周期之间插入trans周期）：

现在，假设允许 master 流水线请求。这意味着下一个fill可以在 4trans个周期完成之前开始：

上面的 SVA 序列无济于事，因为第二次fill它将错误地匹配 4trans个周期，使最后一个trans“浮动”。只有在匹配前一个循环之后，它才需要开始匹配trans循环fill。

该序列需要在单个评估中不可用的全局信息。基本上它需要知道它的另一个实例正在运行。我能想到的唯一方法是使用一些 RTL 支持代码：

trans_ongoing上面的代码应该在事务正在进行时提高该位，并在发送最后一个 atrans_done时在时钟周期中脉冲。（我说应该是因为我没有测试它，但这不是重点。让我们假设它有效。）transfill

有了这样的东西，可以将序列重写为：

这应该可行，但我对我需要支持代码这一事实并不特别兴奋。其中有很多冗余，因为我基本上重新描述了事务是什么以及流水线如何工作的大部分内容。它也不那么容易重复使用。Asequence可以放在一个包中并导入到其他地方。支持代码只能放置在某些模块中并重复使用，但它是一个与存储序列的包不同的逻辑实体。

这里的问题是：有什么方法可以编写序列的流水线版本，同时避免需要支持代码？

给定两个属性P1 = (R1 or R2) |-> P和P2 = (R1 |-> P) or (R2 |-> P)，其中R1和R2是序列 和P是一个属性，说它P1等价于是否正确P2？

我根据 LRM 附件 F 中严格和中性可满足性的定义进行了计算，结果它们是等价的。（我不想排除我在某处犯错的可能性。）

我问，因为我已经看到模拟工具对两者的处理方式不同。

我正在研究 SystemVerilog 断言。我应用 SVA 来检查有效确认规范。规格如下：

当valid被驱动（0到1）时，valid应该等于1，直到ack被驱动（1）。当 ack 被取消断言（1 到 0）时，valid 也被取消断言（1 到 0）。

为了检查这个规范，我写了两个属性（pr1 和 pr2）。您可以从以下链接查看 SVA 代码。 https://www.edaplayground.com/x/5gHd

我预计两个属性的工作原理完全相同。然而，pr2 并没有像我预期的那样工作（我预计断言可能在 50ns 时失败，因为在 50ns 时 valid 等于 1 但 ack 等于 0）。

波形： https ://www.edaplayground.com/w/x/u5

pr2（50ns）有什么问题？

此致，

triggered我有一些使用序列属性的断言。这对于检查“当 X 发生时，Y 必须在过去的某个时间发生”形式的属性很有用。

我们举一个简单的例子：

给定三个信号，a和b，c只有在 3 个周期前为高且2 个周期前为高c时才允许变高。这是满足此属性的跟踪：ab

为了能够检查这一点，我们需要一个辅助（时钟）序列，它应该在 ac合法的点匹配：

然后我们可以在断言中使用这个序列：

这个断言在大多数情况下都可以正常工作，但是在处理重置时它会变得混乱。

假设我们还有一个复位信号，它恰好在b和之间的时钟周期内变为活动状态c：

在这种情况下，天真的方法是在断言之外的default disable iff子句内实现重置意识：

期望是，由于 reset 之前是活动c的，因此a ##1 b之前发生的不计算在内，并且断言失败。但是，这不是发生的情况，因为序列的评估与重置无关。

要实现此行为，必须使序列具有复位意识：

并且断言需要使用重置感知版本：

第二个断言确实会失败，因为two_cycles...由于发生复位，序列将不匹配。

这显然有效，但需要更多的努力，并且需要重置才能成为序列/属性的组成部分，而不是在每个范围的基础上进行控制。在这种情况下，有没有其他更接近于使用的方法来实现重置意识disable iff？

有没有办法在每个时钟周期断言已声明的属性是否为假？

例如，

status[idx]req[idx]只有当两者都为高时才应enable[idx]为高。

我想要的是针对上述情况的负面情景检查器。即当或或低status时，不应该变高。reqenable

我在下面尝试过，但是 vcs 给了我下面的编译错误

错误-[PIWDOAACS] 不正确使用“禁用 iff”

带有 'disable iff' 的属性实例只允许在“assert”、“assume”和“cover”语句中使用。属性 p_RiseIntDischeck 可能不会在此上下文中实例化。

seq_a并且seq_b已经被声明并用于其他一些断言。重用这些序列并为上述情况创建负面场景检查器的最佳/推荐方法是什么？

我有一个嵌套接口，类似于伪示例

我想在interface afrom上写断言interface B

但它不允许我发出alias信号。还有什么其他选择？

有什么建议么？