如何爲異步復位行爲編寫斷言

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);