SystemVerilog 断言：一旦 A 被断言，A 将保持高电平直到 B 被取消断言，之后 A 最终将变为低电平

Question

我试着写了一个断言：

一旦 A 被断言，A 将保持高电平直到 B 被取消断言。之后，A 最终将被反断言。

我写的断言是：

my_assertion : assert property(
    @(posedge clk) disable iff(reset)
    $rose(A) |-> A throughout !B [->1] ## [0:$] !A) 
else $display("Assertion failed")

A 被反断言时断言失败。伙计们，你能告诉我我在my_assertion中哪里做错了吗？ “[0:$]”使用不正确吗？

Answer 1

##的优先级高于throughout；请参阅 IEEE1800-2012 § 16.9 序列操作 Table 16-1.

因此A throughout !B [->1] ## [0:$] !A是样本aA throughout (!B [->1] ## [0:$] !A)。这失败了，因为 A 需要在最后一个周期为高（throughout 的左侧）和低（throughout 的右侧），这将始终评估为 false。

我认为期望的行为是：(A throughout !B [->1]) ## [0:$] !A

Answer 2

我认为您的问题是由于运算符的优先级。当 A 无效时，这不会失败：

$rose(A) |-> (A throughout !B [->1]) ## [0:$] !A

而你写的是一样的：

$rose(A) |-> A throughout (!B [->1] ## [0:$] !A)

永远无法通过，因为A不能同时为true和false。

https://www.edaplayground.com/x/4Vv9

SystemVerilog 断言：一旦 A 被断言，A 将保持高电平直到 B 被取消断言，之后 A 最终将变为低电平

SystemVerilog Assertions: Once A is asserted, A remains high until B is de-asserted, and after that A will finally be low

system-verilog

verification

system-verilog-assertions