インテル基調講演 Form A Mind-Stretcher

プラトン再発行

フォロワー： 0

Synopsys は、Intel Graphics の Dr. Theo Drane による興味深い講演を SolvNet サイトに投稿しました。トピックは、データパスの等価性チェックです。シノプシス VC の正式な DPV の推奨事項のように聞こえるかもしれませんが、いずれにしても視聴する必要があります。これは、日常的なユーザーガイドの種類の売り込みを超えて、より魅力的な領域へと導く、正式な使用法と考慮事項に関する心を拡大する議論です。

フォーマルに関するインテルの基調講演

知的理解とサンプルテスト

あらゆる形態のテスト駆動シミュレーションは優れており、設計仕様や実装の正確性を検証する上でかけがえのないものです。始めるのも簡単です。テストプログラムを作成し、シミュレーションを開始するだけです。しかし、その単純さの裏側は、その必要がないということです。 完全に 開始するために何をテストしているのかを理解してください。私たちは、仕様を注意深く読み、すべてのコーナーケースを理解していると確信していますが、理解を圧倒するほど複雑な複雑さは必要ありません。

フォーマルは、機能を深いレベルで理解することをお勧めします (少なくとも価値のある結果を提供したい場合)。上記の例では、単純な質問 (z がすべて 1 になることはありますか) では、シミュレーターで 188 億サイクルの例を示すことができません。これは極端なコーナーケースであるため、当然のことです。正式なテストでは、XNUMX 秒で特定の非常に自明でない例が提供され、これがそのような唯一のケースであることをわずかに短い時間で証明できます。

OK フォーマルでは、動的テストではできなかったことを実行できましたが、さらに重要なことは、シミュレーターでは決して伝えられなかった可能性があることを学んだことです。その状態が発生する可能性のあるケースは XNUMX つしかないということです。フォーマルは、限られた一連のテストケースにわたる確率論的な要約としてではなく、知的レベルで設計をよりよく理解するのに役立ちました。

仕様の問題

Theo の次の例は、バグ自動販売機に基づいています (ボタンを押すとバグが発生するため、このように呼ばれています)。これは非常に単純な C から RTL への等価性チェックの問題のように見えます。左側が C モデル、右側が RTL モデルです。 Theo が正式な初期の頃に驚いたことの XNUMX つは、gcc が合理的に動作するにもかかわらず、C モデルの右シフト動作が C 標準で完全に定義されていないことでした。ただし、DPV は RTL との比較で不一致について文句を言うでしょう。未定義の動作に依存するのは危険です。

虫自販機としてのフォーマル

C と RTL の仕様比較には、特にビット幅に関して、他の危険が伴います。中間信号のキャリービットの切り捨てまたは損失 (上記の #3) が良い例です。これらは仕様の問題ですか？おそらく、仕様と実装の選択の間の灰色の領域です。

同等性チェックを超えて

DPV の主な目的は、C または RTL リファレンスと RTL 実装の間の同等性をチェックすることのようです。しかし、その必要性は比較的まれであり、そのような技術を適用できる他の便利な方法があります。最初は実装の世界で古典的でした – 変更を加え、バグを修正しました – その結果、新しいバグを導入しましたか? クロックゲーティングを追加した後の SEQ チェックに少し似ています。ブロック出力の到達可能性分析は、場合によっては別の有用なアプリケーションになる場合があります。

等価性チェックだけでなく

テオはさらに創造的になり、研修生に反例を使用して設計をよりよく理解するように依頼し、数独を解く or 整数を因数分解する. 彼は、DPV がそのような問題にアプローチするための奇妙な方法であることを認めますが、彼の意図は、DPV が等価性チェックのためだけであるという幻想を壊すことであると指摘します。興味深いアイデアであり、そのような課題を考え抜くことは確かに脳を伸ばします. (私は、彼が数独の問題について言及した直後に、すぐに数独の問題について考え始めたことを告白します。)