SystemVerilog 断言不会在应该失败的时候失败答案

【问题标题】：SystemVerilog Assertion does not fail when it shouldSystemVerilog 断言不会在应该失败的时候失败
【发布时间】：2023-01-30 00:58:11
【问题描述】：

我有一个简单的断言如下：

$rose(req) |=> !req[*1:10] 直到 ack ##1 !ack;

据我所知，在检测到 $rose(req) 时，断言应检查 !req 是否连续为低电平最多 10 个时钟或 - 直到 - ack 到达（ack=1）。一旦 ack 为真，它应该取消断言下一个时钟。

我的测试从 $rose(req); 开始。然后保持 !req 断言几个时钟（少于 10 个），然后驱动 ack=1。然后，我将 ack=1 保持 4 个时钟。它不会像断言所要求的那样在下一个时钟变低。尽管如此，断言并没有失败。线程“!req[*1:10] until ack”似乎一直在触发，即使在 ack 到达并且满足“直到”条件之后也是如此。

任何想法为什么断言不会失败？

这是模拟场景的 EDA 游乐场链接。

EXAMPLE

【问题讨论】：

标签： fpga register-transfer-level system-verilog-assertions asic

【解决方案1】：

你的断言是完全正确的！

在 !req[*1:10] 阶段，您没有提供有关 ack 信号的信息。

模拟器找到一个序列，其中 req=0 一些时钟周期（最多 10 个），然后找到 ack=1 后跟 ack=0；

你想要的可以通过以下方式获得：

$rose(req) |=> (!ack throughout !req[*1:10]) ##1 ack ##1 !ack;

我不会在这里使用until ack，只是##1 ack

【讨论】：

【解决方案2】：

G.C. 的解决方案有效。

我也找到了另一个解决方案。

@(posedge clk) $rose(req) |=> first_match(!req[*1:10] ##1 ack) ##1 !ack;

【讨论】：