verilog - 简单波形的 SVA 属性

Question

波形：-

我做了一个属性：

property p1;
   a |=> (b == 1)[=2] ##1 (c == 1)[=2]
endproperty

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

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

感谢帮助。

Answer 1

您没有指定在 c 上的脉冲期间 b 不应为 1，也没有指定在 b 上的脉冲期间 c 不应为 1。

那么，这样的事情怎么样：

property p1;
   a |=> ((c == 0) throughout (b == 1)[->2]) ##1 ((b == 0) throughout (c == 1)[->2]);
endproperty

[->N]运算符是精确的非连续重复运算符或goto 重复运算符。使用 goto 重复，表达式必须在匹配的最后一个循环中成立；换句话说，一旦发生指定的重复次数，匹配就实现了。