我想写一个断言，它检查“Valid 应该只在 req 1, ack 1, req 0, ack 0 事务中为高一次”
我想到了以下一个，但它给了我错误。
assert property (@(posedge clk_r) req & ~ack |-> (valid [=1]) throughout ((req & ~ack) ##[1:$] (~req & ~ack)));
有人可以帮我吗？
【问题讨论】：
req-ack 事务的含义。图片不能很好地替代描述，尤其是在没有任何上下文的情况下。
标签： verilog system-verilog formal-verification system-verilog-assertions
我猜“错误”是指编译错误。 throughout 运算符的左侧只能是布尔值，不能是序列。您正在考虑 intersect 运算符。
intersect 将要求其左侧和右侧的序列具有相同的循环数。
intersect 左侧的序列应指定只有一个循环，其中valid 是1。非连续重复操作符是一个好的开始，因为它表示valid 可以从后续匹配开始的时间开始进入任何循环。它没有说明之后会发生什么。它只是说可能存在后续周期，但对这些周期没有要求。
您需要指定valid 是1 的循环之后会发生什么，为了确保valid 是1 的单个循环，我们必须检查valid 是@ 987654333@ 之后的周期。这是使用以下顺序完成的：
!valid [*] ##1 valid ##1 !valid[*]
这可以用几种不同的方式编写，但我发现上面的代码是最易读的。
在结果的另一部分，您可以放心地删除 (req && !ack) 术语并说：
##[1:$] (!req && !ack)
它也没有做我认为你希望它做的事情（检查req 保持1 直到ack 出现）。您应该有一个不同的断言来检查req 应该保持1。这将使调试更容易，因为您将检查 valid 与检查 req 和 ack 分开。
综合起来，断言应该是这样的：
assert property (@(posedge clk_r)
req & ~ack |->
(!valid [*] ##1 valid ##1 !valid [*]) within (##[1:$] (!req && !ack));
注意：您应该使用布尔运算符，而不是按位逻辑运算符。用&&代替&，用!代替~。
【讨论】：
untill_with 搞糊涂了。可以分享最后一个的意思吗？ not 运算符也不同于 ~？
req & ~ack |-> (valid) within (##[1:$] (~req & ~ack));。但它并没有因为交易中的 0 有效而失败。对于 0 个有效交易，断言未完成。所以我们需要相同的东西，但是当 req 0、ack 0 和 valid 没有变成 1 时断言失败
assert property (@(posedge clk_r) valid |=> ~valid[*1:$] ##1 ~req & ~ack);
not 类似于布尔 ! 运算符（我建议使用它而不是按位否定 ~），但它适用于属性。
within 断言不会因为没有valid 的情况而失败。一旦req 和ack 都变低，结果应该停止匹配。