如何为异步复位行为编写断言

Question

让我们举一个简单的例子，说明异步复位的d触发器。

q应该在时钟的下一个边沿上用d更新，这可以用简单的蕴涵算子断言来写。

但是如何在断言中捕获重置行为。 我试过以下几条

assert @(posedge rst) (1'b1 |-> !Q); 

assert @(posedge rst) (1'b1 ##0 !Q); 

这两个断言失败了，我想这是因为第一个没有未来posedge？

assert @(posedge clk) ($rose(rst) |-> !Q); 

通行证，但需要自由运行的时钟，并且时钟的2个边之间有效（未安inteded的第一个行为）

assert #0 (not (rst & Q)); 

按我的理解，这是一个正确的立即断言，不过，我可以看不到这个波形查看器通过/失败。更进一步，我认为我不能在最后一种断言中写封面。

Answer 1

断言失败，因为Q在更新前被采样。抽样发生在触发事件的LHS上，早在模拟器的调度程序中。 Q在调度顺序中后面的反应区域中更新。

解决此问题的简单方法是添加一个微小延迟，如SystemVerilog的1step。我建议将rst置于可用作最小脉宽检查一部分的检查条件中。

wire #(1step) rst_delay = rst; 
assert @(posedge rst_delay) (1'b1 |-> rst && !Q); 

如果您正在使用一个复位到Q延迟模拟，如从SDF注解或人为延迟，则偏移添加到rst_delay。

wire #(r2q+1step) rst_delay = rst; 
assert @(posedge rst_delay) (1'b1 |-> rst && !Q);