问题标签 [system-verilog-assertions]

我正在尝试做这样的事情：

这里c不是一个“常数”，而是一个来自寄存器某些位的值。eg:reg[4:0]只写一次。检查是否b仅在 a 为高“c”个周期时才被断言。

但是，SVA 不接受这样的变量 : [*reg[4:0]]。有任何想法吗？？

我一直无法找到[->]表达式的含义。我熟悉使用范围作为[a:b]或序列，例如EVENT1|->EVENT2，但不熟悉我在开头提到的那个。

上下文是一个断言属性，可确保在复位为低电平时 clk1 始终处于切换状态。

关于[->]真正含义的任何想法？

提前致谢！

我看到断言总是与时钟的 n 个周期有关。有什么办法可以检查时间刻度的持续时间吗？意义

假设我想检查复位是否保持 100ns 或更短，我们如何为此编写断言语句？

我想在 SVA 中编写一个属性来正式验证一个行为。

这是我想要的：

如何重写上述属性，以便在 sig1 下降后，它在剩余的评估周期内保持低电平？

注意：我不想将 sig1 设为禁用 iff (sig1)

在架构中的功能为：

我想验证这个函数的行为是否符合预期。所以我在我的 SVA 文件中写了一个类似（不精确）的函数。

但我得到一个错误：“外部参考函数仍未解决”

如何在我的断言文件中添加外部引用？

我想iff sig1=1'b1在第一个时钟周期后禁用该属性。

从高到低的转变sig1是我的触发条件。如果我这样做disable iff(sig1)触发条件将不会被满足。

throughout在正式验证器中的启用和满足序列上也无法使用。

我该怎么做？谢谢！

波形：-

我做了一个属性：

但是此属性不适用于此波形，它不适用于“c”之前的 3 个或更多“b”，并且不适用于第一个“b”之后的“c”。

我需要一个属性，它可以在“a”信号之后仅传递 2 个“b”，并且仅在“2 c”之后传递，它们之间有任意数量的间隙。

感谢帮助。

我想断言，如果在当前周期信号'a'等于“0110”（二进制）在下一个周期信号'b'不大于31（它应该在0和31之间。它应该小于00000000000000000000000000011111）（它的宽度等于 32）每个人都可以帮我写断言吗？！请原谅我的英语不好。

我想检查变量的当前值是否为“1”，那么变量的先前值应该为“0”。我在系统 Verilog 断言中使用 $past。在这里，我正在检查 cal_frame_mode = 1，然后它是 cal_frame_mode = 0 的先前值。我的代码如下。但是，我看到断言失败。当我检查波形时，它的行为正确。断言在第一次检查后标记 2 个时钟。仅检查一个时钟周期后如何停止此断言？

我是一个基于断言的验证新手，试图了解它应该如何正确完成。我已经找到了很多关于 systemverilog + 断言的结构和技术细节的信息，但我仍然没有找到某种关于在现实世界中如何真正完成事情的“食谱”材料。

问题和限制：

• 设计有一个带有数据、有效和id输入的数据输入总线
• 一个数据“包”是3个样本
• 在通道n之后，总会有来自通道n+1的数据
  • 频道 ID 将在最大 ID 发送后回绕
• 数据字节之间可以有任意数量的 clk 滴答声

• 下面是带有通道 ID 的简单且希望正确的时序图：

  

那么如何用最少的代码做到这一点呢？干净整洁。以前我已经构建了虚拟 verilog 模块来驱动数据。但是可以肯定的是，可以只使用一些假设属性来限制通道 ID，否则可以腾出手来让正式工具尝试破坏我的设计？

初学者的简单模板可以是：

我想问题是像上面这样的假设/断言往往会在每个数据样本上触发并创建时间重叠的并行线程。