让我们举一个带有异步复位的广告触发器的简单示例。
q 应该在时钟的下一个边沿用 d 更新，这可以用简单的蕴涵运算符断言来编写。
但是如何在断言中捕获重置行为。我试过以下几个
assert @(posedge rst) (1'b1 |-> !Q);
assert @(posedge rst) (1'b1 ##0 !Q);
这两个断言都失败了，我认为是因为没有 rst 的下一个姿势？
assert @(posedge clk) ($rose(rst) |-> !Q);
通过但需要自由运行的时钟并在时钟的 2 个边沿之间断言（不是 rst 的内置行为）
assert #0 (not (rst & Q));
根据我的理解，这是一个正确的直接断言，但是我在波形查看器中看不到这个通过/失败。此外，我认为我将无法为最后一种断言写封面。
断言失败，因为Q在更新之前对其进行了采样。采样发生在触发事件的 LHS 上，在模拟器调度程序的早期。Q在调度顺序后面的反应区域中更新。
纠正这个问题的一个简单方法是添加一个微小的延迟，例如 SystemVerilog 的1step. 我建议放入rst可以作为最小脉冲宽度检查的一部分的检查条件。
wire #(1step) rst_delay = rst;
assert @(posedge rst_delay) (1'b1 |-> rst && !Q);
如果您使用 reset-to-q 延迟进行模拟，例如使用 SDF 注释或人工延迟，则将偏移量添加到rst_delay.
wire #(r2q+1step) rst_delay = rst;
assert @(posedge rst_delay) (1'b1 |-> rst && !Q);