將SystemVerilog聲明延遲轉換爲invarspec

Question

我想將延遲的SystemVerilog聲明轉換爲正式驗證者的invarspec。合成器在下面的代碼行中給出## 1的語法錯誤。

assert property ((req1 == 0) ##1(req1 == 1) ##1 !(req2 == 1) || (gnt1 == 0)); 

有幾個屬性需要驗證並有延遲。我目前正在嘗試使用合成器將它們轉換爲正式（SMV）模型規範，該合成器適用於不涉及延遲的屬性。我可以模擬這種形式驗證工具的延遲嗎？如果是這樣，怎麼樣？

Answer 1

一種方法是在Verilog中顯式建模信號的延遲版本，然後您可以使用沒有時間依賴性的斷言。

對於示例：

assert property ((req1 == 0) ##1(req1 == 1) ##1 !(req2 == 1) || (gnt1 == 0)); 

變爲：

reg req1_r,req1_rr; 

always @(posedge clk) begin 
    req1_rr <= req1_r; 
    req1_r <= req1; 
end 

assert property (!((req1_rr == 0) && (req1_r == 1)) 
       || !(req2 == 1) || (gnt1 == 0));