JasperGold初心者サポート記(東アジア編)
東アジアのお客様訪問の話をします。現在、初めてフォーマル検証に挑戦しているユーザ様のサポートをしています。これまでは、UVM (Universal Verification Methodology)でシミュレーション環境を構築し検証をしていたようです。
フォーマル検証で最も重要なのは、DUT(Design Under Test)の機能要求を理解し、検証プランを立て、プロパティで表現できるところまで落とし込む作業です。初心者のお客様対応でもここに最も時間をかけます。プロパティに不慣れなお客様には書き方もお伝えします。インプリケーション A |=> Bや、関数 $stable(), $fell() などの基本的な文法で十分です。その後、アサーションやアサンプションの使い分け、JasperGold® の使い方説明になります。
今回も検証プランを議論し始めると、お客様が今まで慣れたシミュレーション的な発想で「このレジスタをセットした時にこの信号がHighになると、この条件の時にこの出力信号がこうなる事を検証したい、どうすれば良いか?」などと聞いてきました。日本や東アジアにかかわらず、初心者のお客様の場合、だいたいこのあたりからのスタートです。お客様に、「もっとハイレベルな視点でこの回路の振る舞い、機能仕様を教えて欲しい」とお願いしました。「こういうプロトコルのインターフェースがあり、このブロックがこれを要求すると、あのブロックに要求が転送され、ここで別のハンドシェークをしてタスクが終了する」などと、分かりやすく説明をしていただけました。お客様によっては、波形とにらめっこするだけで、いつまでも実装仕様や特定の信号の振る舞いから脱出できず、機能仕様を説明できない場合もあります。いわゆる「機能仕様書が無い事件」です。今回のお客様の所では、問題になりませんでした。その後、機能仕様から具体的な検証プランまで落とし込みます。ドラフト案は私が持ち込みました。いつものように、検証する機能をプロパティで表現するために、補助回路を用いました。補助回路も検証プランの一部で、多くの場合とても重要です。補助回路のことを英語ではGlue Logic (糊付け論理)と呼び、カウンタやフラグ、またはステートマシンで作るのが一般的です。このステートの時にその信号は変化できる/できない/この値をとる、などの要領でプロパティ仕様をホワイトボードに書き上げます。検証プランの出来上がりです。細部を見れば、最初にお客様が言っていた「このレジスタをセットした時にこの信号がHighになると...」も検証できます。
ハイレベルな視点で機能仕様から検証プランを立てると、プロパティ表現に必要なコード量も少なくなります。レビュにおいても、どの機能をどう検証しようとしていて、どのプロパティが何に対応しているかが分かりやすくなり、結果、検証の品質が高まります。このような検証手法の議論や雑談も交えながらの作業です。そして、お客様は初めてのフォーマル検証環境をスクラッチから書き上げました。コーディング作業は、トータルで実質2時間もかからない程度です。そこに至るまでの仕様の理解、検証プランの立案や修正、それらを理解するための議論のほうが作業時間の中で支配的です。検証プランが全てだといっても過言ではありません。
JasperGold を用いて証明を実行すると沢山のカバープロパティがフェイル(到達不能である事が証明される)し、アサーションもフェイルしました。次に、これらフェイルの解析方法の説明に移りました。
アサーションのフェイルは、波形を見ることができます。この波形のことを、反例とかカウンターエグザンプル(Counter Example, CEX)と呼びます。反例の解析は、当然ですが波形があるので比較的簡単です。波形やRTLを参照しながらシミュレーションと同様の解析手法で原因を特定します。JasperGoldには高機能な波形ビュアのVisualize™️があるので、これを用いてデバッグの仕方を説明しました。
一方、カバープロパィがフェイルした場合は、問題を観測する波形がありません。反例波形がある場合とは問題解析方法は異なります。カバープロパティがフェイルする原因は下に示すように、いくつかあります。
1. RTLが原因(設計バグの可能性)
2. カバープロパティ記述ミスが原因 注釈1
3. 検証環境に追加した制約、アサンプションで過剰制約状態になったことが原因
お客様には、上記3の過制約から疑うことを提案しました。環境を制約しているアサンプションを環境から切り離し、カバープロパティのトレース波形が見つかれば、そのアサンプションが過制約を起こした可能性があります 注釈2 。同アサンプションをレビュし、記述が正しいと判断できる場合は、上記1のバグ、または上記2のプロパティの記述ミスを疑います。この辺りは、フォーマル検証に特有の概念なので、お客様とも比較的長い時間をかけて議論しました。
お客様のサポートは現在も継続中です。最後の訪問では、バグらしき波形を見つけました。仕様ではDUT内の制御レジスタ設定に依存して命令を無視するはずですが、特定の制御レジスタを変更すると無視されるはずの命令が処理されてしまう反例を、 JasperGold が見つけたのです。「多分、シミュレーションではみつからない」と驚いていました。このお客様は、もう初心者ではありません。海外出張ベースでここまで2ヶ月程対応してきましたが、オンサイトで対応できる日数はかなり限られています。お客様本人も、フォーマル検証以外にUVM環境を構築してシミュレーションによる検証をしていてフォーマル検証に割り当てられる時間はまだ少ない状況です。これらを考慮しても、ここまで達成できたのはとても早いと思います。お客様がとても優秀であることも理由にありますが、フォーマル検証だから為せる技とも言えます。
JasperGold は東アジアのお客様にもとても好評で、上述したように積極的に学び導入している状況は、日本人の私には驚異にも思えます。日本のお客様の中には、実績のある社内の独自ツールの使い回しやこれまでの手法を守りつづける事が正しいとする現場もあると聞いています。中には、ツールにやらせると人が育たないという理由で、長時間かかる非効率なマニュアル作業を社員に強いる部署もあるようです。一方、これまで日本企業を追いかけてきた外国企業は、過去のしがらみが比較的少ないからか、新しい手法を先入観なく導入しやすいのかもしれません。結果として、多くの若いエンジニアが高い品質のまま効率よく検証するスキルを身につけています。ツールに任せられる仕事はツールに任せ、余った時間でよりハイレベルの仕事を人が担当できるようになります。はい、今回も前回執筆した「東アジアのお客様は英語の資料を要求してきましたよ」(リンクはこちら)と同様に、皆様のお尻を叩くつもりで、この記事を書いています。近い将来、世界から「フォーマル検証といえば日本」と言われるように、JasperGold が日本のハードウェア検証技術を底上げし、日本の半導体業界を盛り上げるきっかけになれれば最高です。日本ケイデンスには、フォーマル検証に精通した優れたAEが沢山います。お客様の部署の初心者教育に関しても、是非お気軽に相談してください。
最後に、この場を借りまして、フォーマル検証イベントのお知らせがあります。2018年12月5日、イノテックビル・セミナールーム(新横浜)において本年度のClub Formal を開催いたします。詳細は後日、弊社ホームページ等でお知らせいたします。
- JasperGoldでは、アサーションやアサンプションに用いているプリコンディション(Precondition)のカバープロパティを自動で生成する機能があります。これらプリコンディションの表現ミスも検出することが可能です。
- JasperGold では、自動的に過制約を引き起こしている可能性のあるアサンプションをレポートする機能もあります。
Verification Customer Enablement
Sr Principal Customer Engagement Engineer
渡口和信
この記事に関する問い合せ先:
コーポレート・マーケティング部
E-mail:cdsj_info@cadence.com
Latest Issue
- 【Power User’s Voice】 壁を破壊せよ!FinFET対応の設計フロー、回路設計とレイアウト設計との融合
- Palladium-Joulesによる高速・高精度なシステムレベルパワー解析の実現
- 共通設計環境Stylusを使ってデジタル設計を効率化しませんか?
- 1000 CPUまで高いScalabilityを維持してFSで容量抽出が可能 – Massive Parallel Quantus FS(3D Field Solver)
- Virtuoso ICADVM18.1 - 先進的メソドロジーご紹介
- 「Correct by Design」で効率化を実現するAllegroソリューション
- 編集後記
Archive
2023 Issues
2022 Issues
2021 Issues
2020 Issues