シーケンシャル等価性検証 (つづき)

3. シーケンシャル等価性検証

私には一抹の不安があります。私が前回説明したシーケンシャル等価性検証の特徴を理解されていない方が沢山いるのではないかということです。気になりだすと切りがありませんので、次に進む前にここでシーケンシャル等価性検証ではどのようなことができるのかを例をどんどん示したいと思います。回り道は始まったばかりです。

1. と言うことで、いきなりのSystemCの例題です。これが何を意味しているのか理解できないという人は、SystemCの入門書や、おそらくこのSystemC Japan オフィシャル･サイトのどこかにある情報で勉強が必要です。しかし、今はそんなことはどうでもよいのです (SystemCサイトなのに大丈夫なの?!)。その様な人も、さあ自信を持って進みましょう。

この記述は、4つの入力を全て加算して出力するものです。組み合わせ回路ですね、格好よく言えばuntimeなアルゴリズム記述です。この等価性検証をSLECでしてみましょう。何と等価性を取るの？ それ自身とです。そんな意味のないことを!! と思った人、リッチー&カーニハンの「The C Programming Language」でも最初は”hello, world”なのです!!

これが、SLECの”hello, world”に相当する検証スクリプトです。我々はこれをプロブレム･セットアップ(problem setup)と呼びます。ここでの大事なことは２つあります。

build_designというコマンドでデザインを2つ読み込み、それぞれに-specと-impl(以後SPEC、IMPLと略す)という名前を振って2つのデザインを識別させます。SPECとIMPL以外の名前をつけることはできません。しかし単なる名前ですので、どちらをSPECにするかは自由ですし、入れ替わってもできる事に変わりはありません。そしてverifyコマンドで検証させることが2つ目の大事な点です。

これをSLECに実行させると次のような結果が得られます。Provenと書かれたところが、機能的に一致した数を示しています。Output-Mapsのところが1つProvenですので、1つしかない出力のところで等価が証明されたということを意味しています。Falsifiedは不一致となった数、Not-Attemptedは検証前に処理が終わったもの数を示します。Cond-ProvenとBounded-Provenは、今のところは無視してください。

2. それでは、少しSystemCを変更してみましょう。この新しい記述は最初のものと同じ機能を保っていますか。変更した者としては、その責任を負わなければいけません。ということで続いてSLECで検証してみましょう。
   

ここで大事なことは、SLECの検証スクリプトにlatencyという概念が登場してきたことです(青時部分)。SPECとしては、最初の記述を読み込んでいますから組み合わせ回路ということでlatency=0です。Latency=0はデフォルト設定ですので、ここでは明示的に指定する必要はありません。最初のSystemC記述同士を用いた検証でも、このデフォルト値が用いられています。

新しい記述は加算出力のところにレジスタが挿入されるので、1サイクル遅れの出力となりlatency=1です。以下の図を参照してください。それ以外にも検証スクリプトに色々と追加されていますが、それらはリセットに関する記述です。今のところ無視しておいて問題ありません。

結果は次の通り。今回の検証では、IMPL側がlatency=1と仮定した場合、2つのデザインは機能的に等価であることが証明されました。つまり同じタイミングで同じ値を２つのデザインに入れれば、latency=1の差こそあれ常に同じ値が出力されることを意味しています。

3. 更に変更しましょう。今度は、パイプライン動作にしてみました。あまり美しい記述とは言えませんが、動作としては問題ありません。

さて検証スクリプトは次のようになります。SystemC記述の変更に比べれば、検証スクリプトの変更箇所は少ないですね。正確に言えばIMPLのlatency=3の部分が変わっています。その理由は、SystemCのパイプライン動作が3段で構成されているからです。

この検証を図で表すと以下のようになります。

そして、念のために波形で確認してみましょう。

4. 更にSystemCの記述を変更して、加算器を共有化してみます。排他的に4サイクルを一つの処理期間として、4つの入力の全ての加算に割り当てています。1サイクル目の入力ラッチから4サイクル目の演算結果の出力までがあります。Compute()内のwhile loopには４つのwait()文がありますが、これにより暗黙的に4つの状態をもつFSMを構成し、それぞれの状態で処理する内容を記述しています。

このSystemC記述を見て、色々とご指摘のある方がいらっしゃるかもしれません。私からひとつ挙げるとすると、厳密には加算器の共有化がされていない点があります。ソースコード上で共有化の雰囲気だけ醸し出しています。しかし、ここでは正しく動作が表現できていれば等価性検証のことを知るには充分ですので、SystemCの細かなことは気にせずにSLECの検証スクリプトを見ていきましょう。

ここでは、新しくthroughputという概念が出てきました。一連の処理にかかるサイクル数をthroughputで定義します。今回のSystemC記述では、throughput=4です。SPEC側は最初の記述ですので組み合わせ回路です。ここではデフォルト値のthroughput=1を持っています。この場合の解釈は、1サイクルごとに新しい入力を得るとしてお茶を濁しましょう。

更に今回のSystemC記述はlatency=4となっています。データ入力から4サイクル後に結果が出力されるのですから、そのような値を取ります。検証結果は次のようになります。

この検証を図で表したものと、波形による検証意図の確認を示します。

さて、これまで4つの異なるSystemC記述を見てきましたが、これらは全て機能的に等価でした。これらは順序回路としてみた場合、内部の構造は異なっています。しかしシーケンシャル等価性検証ツールであるSLECは、それらの違いを乗り越えて等価性の証明を行っています。

SLECは全ての順序回路をトランザクションという共通の抽象的な時間に割り当ててから検証を行うので、内部の構造が変わっても、処理のタイミングが異なっても対応できるのです。トランザクションはlatencyとthroughputによって定義されます。

さあ、いよいよトランザクションの本質か!!と期待された方、残念ながら回り道はそれほど簡単には終わりません。次回も引き続きシーケンシャル等価性検証、SystemCを更に変更していきながらSLECでそれを検証します。乞うご期待を。

1 | 2 | 3 |