JasperGold で 仕様書が書きたくなる
検証をする皆様の多くは シミュレーションを用いたダイナミック検証に慣れていると思います。
私もSpecman®を使ったカバレッジドリブンで制約付きランダム検証を長年行ってきました。その頃から、単体(ブロック/ユニット)検証をどの階層からやれば効果が高いのか、SOCのIPレベルかその下のブロックレベルかを同僚と議論し、複数の プロジェクトで試してもいました。
この議論は、JasperGold®をどの回路に適用すると最も効果的か、という議論にも似ています。ただし、シミュレーションとフォーマル機能検証(以下、フォーマル)に必要な条件が異なるので、その答えも当然変わるはずです。フォーマルではDUT (Design Under Test)への入力信号をドライブする必要がないため、BFM(Bus Function Model)やDriver が要らないことから検証環境構築に必要な工数がシミュレーションの場合と比較して短縮できます。結果、今までシミュレーションでは躊躇していたより下位階層の検証で、早期にバグを見つけるシフトレフトが期待できます。
シミュレーションにおける課題
シミュレーション時に、ある階層より下の回路の機能検証を行わない理由を考えます。多くの場合、現場では、
1. この階層で、回路の機能仕様書がない(書く時間がない)
2. 独自インターフェースを有し、入力をドライブする検証IPがない(作る時間がない)
つまり、検証をするために必要な仕様や環境を作る時間が作れないことが主な理由ではないでしょうか。わざわざ検証しても、費用対効果が悪いという判断だと思います。同様に、
3. 上位階層で検証するから(この階層なら仕様書もあるし環境もある)
という理由で、軽視されるかもしれません。その階層で検証しないので仕様書がなくても仕方がないとされます。これが慢性化すると、仕様書がないことが当たり前になります。
一方で、下の階層で 検証をしなかったことで、本来ここで比較的簡単に見つかるであろうバグがあっても、上位階層で見つけようとした時に、
· バグにヒットするための入力パターン生成がより運まかせになる
· 下位階層を包括した機能カバレッジゴールの定義が難しい
· ゴール定義ができても、上位階層でやるほど達成が困難になる
· 運良くバグを見つける事ができても、下位階層でやるより修正に必要なイタレーションに時間がかかる
などの課題が出てきます。皆様も経験済みのはずです。
これらを解決する方法の一つに、「下位階層で検証をする」がありますが、上述したように下位階層でやらない現場の理由もあるので、ここに負のループがあります。
フォーマル機能検証のメリット
フォーマルでは、DUTへ入力する信号をドライブする必要がありません。入力と出力のプロパティ(制約やチェッカ)があれば十分です。シミュレーションと比較して、検証環境を作る工数が大幅に削減できるメリットがあり、その効果は絶大です。
つまり、もし機能仕様書があり、これをベースにプロパティが書ければ、場合によってはスクラッチからでも検証環境が数時間で構築でき、すぐにバグを見つけることもあります。この検証のスピード感を一度体験すると、フォーマルで検証するために仕様書を書くモチベーションは高まると思うのです。ユーザー時代の私は、少なくともそうでした。まだ体験したことがないというお客様には、是非、仕様書がある回路で、JasperGold を試していただいて、その効果を実感してほしいです。
もちろん、そのために、プロパティを書くスキルも課題になる場合があります。でも大丈夫です。簡単なコツをさえわかれば、 誰でも簡単に書くことができます。例えば、startパルスに対して done パルスがそれぞれ1サイクルずつ発行されるハンドシェークの場合であれば、1 bit のflag を検証環境に追加すれば、assume start |-> !flag のように(詳細は図1を参照)簡単に書くことが出来ます。
図1:プロパティの記述例 ( start と done によるハンドシェーク)
さらに複雑な仕様なら、今回用いた1 bit の flag の代わりにカウンタやステートマシンを使えば、プロパティの表現力も増します。プロパティ記述は、シミュレーションに必要なDriver やBFMを作るのと比較すると、とても簡単です。
このように、JasperGoldを使う選択肢があると、シミュレーションと比較して検証環境が簡単に作ることができるので、下位階層の回路でも、わざわざ仕様書を書いて検証しようというモチベーションが高まると思います。
まとめ
フォーマルにまだ慣れていないお客様であれば、いきなりIPレベルで適用するよりは、もう少し下の階層で試していただくことをおすすめします。この手法は、 複雑な問題を複数のより簡単な問題に分割する一般的な問題解決法で、Divide and Conquer と呼ばれています。シミュレーションでは下位階層の検証環境を作る時間がないことで今までは躊躇していた、組み合わせやタイミングが複雑でバグが沢山ありそうな新規開発の回路こそ、フォーマルのスイートスポットと言えます 。
一方で、Divide and Conquer をやりたくても仕様書がないから検証できないという課題もあります。JasperGold で素早くバグを見つける面白さや効果を知れば、仕様書を書くモチベーションは高まると思います。そしてある程度フォーマルに慣れた後に、より上位階層のターゲットをDUTに選び、収束問題を解決するために抽象化やNondeterminism を使った検証プランを学ぶというステップを踏むのは、とても良いと思います。
Divide and Conquerに関しては、2017年の11月に弊社のサンノゼ本社で開催された JUG (Jasper User Group Conference) で、Hewlett Packard 社フォーマルチームリーダーの Jim Kasak 様や、Samsung Advanced Computing Lab のRajesh Rathi様が、その発表中でも紹介しています。是非、こちらもご参考にして下さい。
Club Formal Japan 2018
2018年2月1日に新横浜でClub Formal を開催しました。「フォーマルのROIを高めるターゲット選択、その課題と対策の議論」のセッションで、仕様書の重要性や Divide and Conquer の考え方を紹介させて頂きました。お天気の悪い中、ご参加頂いた皆様、ありがとうございました。
フィールドエンジニアリング&サービス本部
Jasper R&D, Sr Principal Product Engineer
渡口 和信
この記事に関する問い合せ先:
コーポレート・マーケティング部
E-mail:cdsj_info@cadence.com
Archive
2023 Issues
2022 Issues
2021 Issues
2020 Issues