FC2カウンター FPGAの部屋 OVL(Open Verification Library)を試してみる3(アサーションの説明)
FC2ブログ

FPGAやCPLDの話題やFPGA用のツールの話題などです。 マニアックです。 日記も書きます。

FPGAの部屋

FPGAの部屋の有用と思われるコンテンツのまとめサイトを作りました。Xilinx ISEの初心者の方には、FPGAリテラシーおよびチュートリアルのページをお勧めいたします。

OVL(Open Verification Library)を試してみる3(アサーションの説明)

はじめの一歩-テストベンチ-”に書かれているassert_range アサーションはある信号の値が自分の意図する範囲に入っているのかを確認するアサーションだ。アサーションとは、検証する必要のある設計意図としての動作、つまりプロパティに対する記述分だそうだ。(アサーションベース設計、原書2版、第1章はじめに、4ページより引用)つまりRTLで動作を記述するのだが、RTLではいろいろなステートマシンやその他のカウンタやロジックなどが複雑にからみ合って記述する必要がある場合がある。その信号だけを考えてみよう。その場合に、その信号は例えば4ビットのバイナリなんだけど、10進数を表していて、取りうる値の範囲は0~9までという設計だったとしよう。多分、このRTLコードには、間違いは少ないと思うが、その信号のプロパティとしての値の範囲は0~9ということを検証しようとする。そのときに使えるのがアサーションということになる。アサーション記述言語には、OVL、PSL、SystemVerilogアサーションの3つが有名らしいが、そのうちのPSL、SystemVerilogアサーションは対応するシミュレーターが必要となる。OVLはライブラリとしてコンパイルすれば、どのシミュレーターでもアサーションを記述することができる。
これまで、アサーション記述言語のことを書いてきたが、Verilogでもアサーションを書くことができる。例えば、キャラクタ描画テスト回路のFIFOのoverflow, underflowが出ているかどうかを見るために、シミュレーション限定でVerilogコードによるアサーションを書いてあった。本来、FIFOのoverflow, underflowは起こらないように制御するものであるが、制御コードのバグによって起こってしまう場合がある。アサーションによってそれを監視していれば、起こった時にすぐわかるわけだ。それが分からないと、なかなかデバックが難しくなったりする。下に示すのは、ビットマップVGAコントローラに使用した非同期FIFOのアサーションだ。この非同期FIFOには、underflow, overflow端子を生成しておいたので、それがアサートされるかどうかをチェックしている。

    // アサーション
    // synthesis translate_off
    always @ (posedge clk_ddr2) begin
        if (reset_ddr2)
            ;
        else
            if (afifo_underflow) begin
                $display("%m: at time %t ERROR : FIFOが空なのにリードした",$time);
                $stop;
            end
            if (afifo_overflow) begin 
                $display("%m: at time %t ERROR : FIFOがフルなのにライトした",$time);
                $stop;
            end
    end
    // synthesis translate_on


ちょっと日本語になっているのが微妙ですが、Veritak用ということで。。。
これだけだが、これでunderflowやoverflowを検出できてずいぶんと助かった。
さて、OVL V1でこれをやろうとすると、assrt_neverを使うのだろう。上のVerilogアサーションと等価に書くには、下のように書けば良いと思う。

    // アサーション
    // synthesis translate_off
    assert_never #(`OVL_FATAL, 0, "ERROR : FIFOが空なのにリードした") fifo_underflow_assertion(clk_ddr2, ~reset_ddr2, afifo_underflow);
    assert_never #(`OVL_FATAL, 0, "ERROR : FIFOがフルなのにライトした") fifo_overflow_assertion(clk_ddr2, ~reset_ddr2, afifo_overflow);
    // synthesis translate_on


上の記述は確かめていないので、動くかどうかわかりません。あくまでもイメージということでお願いします。(動かなかったら教えてください)
というわけで、数行に渡っていたVerilogのアサーションがOVL V1を使うと、1行で書くことができる。こんな簡単なアサーションだけではなく、例えば、requestとackの関係はassert_nextによって検証することができる。

次はassert_で表されるOVL V1のアサーションをovl_で始まるOVL V2のアサーションに書き換えてみる。OVL V2は、機能が拡張されていて、OVL V1を含んでいるそうだ。

  1. 2010年03月11日 23:17 |
  2. アサーション事始め
  3. | トラックバック:0
  4. | コメント:0

コメント

コメントの投稿


管理者にだけ表示を許可する

トラックバック URL
https://marsee101.blog.fc2.com/tb.php/1402-1ce28eaf
この記事にトラックバックする(FC2ブログユーザー)