SVA - アサーション、なにそれおいしいの？

はじめに

アクセス解析によると本ブログで1つしかないSVAの記事を引っ掛けてくれる方が多いようです。というわけで今日はアサーションネタいってみます。

こんにちはアサーション

アサーションって導入できたチームとできないチームが極端に分かれそうな検証手法のような気がします。食わず嫌いなチームの言い分はこんなではないでしょうか？

• ウチはホワイトボックス検証なんかしないよ？
• アサーション書けるほど実装仕様書ないよ？
• アサーション誰書くの？
• 書いたプロパティが正しいかレビューするの大変だよ？
• そもそSVA書ける人、読める人がいないよ？
• 今までの検証だけでも大変なのにに更に追加でアサーションなんて工数ないよ？
• 等々

なーんてそんなこと言っていても始まらないので、まずは適当なアサーションを書いてみたいと思います。

DUT仕様

適当なハンドシェイクするDUTを考えます。
仕様は、reqが1パルス入力されると2サイクル後ackを1パルス返します。
テストベンチ側から見た波形はこんな感じです。

これを確認するプロパティを考えてみます。

プロパティその1･･･レベルで確認

property sva_req_ack_pass1 (clk, rst_n, req, ack);
    @(posedge clk) disable iff(!rst_n)
    req |-> ##2 ack;
endproperty

プロパティに書かれた内容はこんな感じです：

• リセット=0でないときにdisable iff(!rst_n)、req=1reqならプロパティを発動して|->、2サイクル後##2に、ack=1ackかを確認する。

実行すると、無事アサートされてパスします。

プロパティその2･･･片エッジで確認

プロパティその1はreqとackがレベルとして1であるのことだけを考えたプロパティでした。プロパティその2では立ち上がりを意識したプロパティを書いてみます。信号の立ち上がり検出には$rose()を使います。

property sva_req_ack_pass2 (clk, rst_n, req, ack);
    @(posedge clk) disable iff(!rst_n)
    $rose(req) |-> ##2 ack;
endproperty

プロパティに書かれた内容はこんな感じです：

• リセット=0でないときにdisable iff(!rst_n）、reqが立ち上がり$rose(req)ならプロパティを発動して|->、2サイクル後##2に、ackの立ち上がり$rose(ack)を確認する。

実行すると、無事アサートされてパスします。

プロパティその3･･･両エッジで確認

次のプロパティでは、プロパティその2に更に信号立ち下がりを意識したプロパティを書いてみます。信号の立ち下がり検出には$fellを使います。

property sva_req_ack_pass3 (clk, rst_n, req, ack);
    @(posedge clk) disable iff(!rst_n)
    $rose(req) |-> ##1 $fell(req) ##1 $rose(ack) ##1 $fell(ack);
endproperty

プロパティに書かれた内容はこんな感じです：

• リセット=0でないときにdisable iff(!rst_n）、reqが立ち上がり$rose(req)ならプロパティを発動して|->、1サイクル後##1に、reqの立ち下がり$fell(req)を確認し、1サイクル後にackの立ち上がり$rose(ack)を確認し、1サイクル後にackの立ち下がり$fell(ack)を確認する。

実行すると、無事アサートされてパスします。

プロパティその4･･･レベルとエッジでもっと確認

今回のDUT仕様ではreqとackが排他にアサートされることが伺えます。最後に2つの信号の関係を意識したプロパティを書いてみます。

property sva_req_ack_pass4 (clk, rst_n, req, ack);
    @(posedge clk) disable iff(!rst_n)
    $rose(req) |->
        !ack ##1 ($fell(req) & !ack) ##1 ($rose(ack) & !req) ##1 ($fell(ack) & !req);
endproperty

プロパティに書かれた内容はこんな感じです：

• リセット=0でないときにdisable iff(!rst_n）、reqが立ち上がり$rose(req)ならプロパティを発動して|->、このサイクルはack=0!ackを確認し、1サイクル後##1に、reqの立ち下がりとack=0$fell(req) & !ackを確認し、1サイクル後にackの立ち上がりとreq=0$rose(ack) & !reqを確認し、1サイクル後にackの立ち下がりとreq=0$fell(ack) & !reqを確認する。

実行すると、無事アサートされてパスします。

で、全部パスしたジャマイカ...osz

はいそうです...osz。今回用意したプロパティは全て正常動作をカバーしています。テストベクタでは典型的な正常動作だけだったので全てパスします。ですが、NG動作なテストベクタを入れた場合にどうなるか...NG時に発火するものとしないものとがありそうなのがなんとなく想像できますよね。
結局のところ何をチェックするか、に応じてプロパティを正しく書く必要があるわけです...そんなの知ってるyo!

今日はここまで

アサーションのプロパティって何を確認するか、にあわせてプロパティを書きたいですよね...自分は無理ですが！ なお、今回使った全ソースは次の機会に準備しようと思います...たぶん。