ハンドシェイク手順の SVA アサーションを作成しようとしています。
私の検索では、次のことがわかりました。
property p_handshake(clk,req,ack);
@(posedge clk)
req |=> !req [*1:max] ##0 ack;
endproperty
assert property(p_handshake(clock,valid,done));
ただし、「完了」信号は、有効なサイクルが高くなった後に何サイクルも来ることが許可されています。このステートメントで、valid がアサートされた後、valid がアサート解除されることなく、任意の時点で "done" がアサートされるようにするにはどうすればよいでしょうか?
$rose(req) |=> req[*1:$] ##0 ack;
$roseの立ち上がりエッジでアサーションを開始しreqます。[*1:$]1 から無制限のクロックの範囲で左辺が真でなければならないことを意味します。[+]と同等の which を使用できます[*1:$]。
チェッカーを記述する他のスタイルは次のとおりです。
$rose(req) |-> req[*1:$] ##1 (ack && req);
$rose(req) |-> ##1 req throughout ack[->1];
有効な $rose のときに、done がまだアサートされていないことを確認するために、SVA も必要ではないですか? もしそうなら、pls はこの SVA を考慮します- $rose(valid) |-> ~done ##1 $stable(~done) [*949:950] ##[1:$] done;
上記では、一定期間アサートされず、その後いつか将来アサートされる必要があります。