遅延を伴う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));