アサーション(SVA)の下書きをしたいときには
筆者が属するグループに最近、アサーションについての相談が何度か寄せられました。アサーションを書こうとするが不慣れで自信がない、練習したい、あるいは記述が込み入って間違いが混入することがある、といったところにお悩みで、助けになるよいツールを探しておいででした。
回答の一つはVerisium™ Debug App (旧Indago™ Debug) 上のTrace Calculatorです。関数電卓のようなインタフェースを持つGUI上でアサーションをコーディングでき、さらに作成したアサーションを現存する波形に対して試し適用できる (シミュレーションを再実行しない) ため、特に既存シミュレーション環境のアップグレードなどに好適です。
もう一つの回答は、Jasper™ Formal Verification Platform(以下Jasper)です。Jasperはアサーションによってデザインを検査するフォーマル検証ツールです。であれば正しいアサーションが用意できる前はまだ出番ではないと思われるかもしれません。実はその印象とは反対に、Jasperが持つフィーチャを適宜利用することで、まったくなにもない状態からアサーションを準備する場合でも強力な助けになるのです。
下の図はJasperの「普通」の使い方、検証を行っている場面です。検証対象デザインにアサーションを取り付け、証明を行い、アサーションがフェイルし、その波形を表示させています。この波形を手掛かりにデザインのバグを探します。
今したいのは、アサーションによる検証ではなくアサーションそのものを練習することでした。ここでそのための簡単なトリックがあります――デザインなしにアサーションのみをJasperに与えて証明するのです。するとJasperが、assert文へのフェイル波形やcover文へのパス波形を提示します。それらの波形を表示させ、納得できたら次の波形、さらに次の波形を表示させて(その間にアサーション記述を修正するかもしれません)、試し書きしたアサーションが意味していることを波形で理解しようという作戦なのです。
実際にアサーションをJasperに読み込ませ、パス波形とフェイル波形を描かせたのが次の図です。パス波形を描かせるのには、assert文を同じ式のままcover文に転換しています(手作業でなくJasperに行わせています。:witness1というcoverがそれです)。
プロパティ式と見比べると、確かにパス/フェイルする波形です。将来このアサーションを検証対象に取り付けたときにも同様、デザインの挙動を監視しパス/フェイルを報告してくれることでしょう。
さてこれらの波形はJasperの証明エンジンが「見繕い」で提示したものです。別の波形を見たくなったら? そこで利用するのが、組み込みの波形ビューワVisualize™ が持つお絵描き機能です。波形をマウスで“修正”して、その修正込みで次なる波形を探させることができます。例えばフェイル波形に対してちょっと悪戯をしてみます――1サイクル目でaがLだったら?(フェイルしないはず…)。実際に得た波形がこちらです。Jasperはなんとしてもアサーションをフェイルさせるべく、波形を2サイクルに延長しました。aがLならフェイルしないはず、という期待が裏付けられています。
式 a |-> b==c はとても簡単なので練習の必要はないでしょう。ただ実際のアサーションはもう少し(あるいはかなり)複雑なことがあります。多くの動作モードを備える回路を検証するときなどは、アサーションから参照するために素のVerilogでセレクタなどをコーディングします(補助コード、グルーロジックなどと呼びます)。補助コード側も動作確認しておきたいですよね。先の例とまったく同じです。Jasperに与え、パス/フェイル波形を表示させ、Visualizeで信号(入力でも、自作した補助コードでも)をプロットし、「ではこの信号が〇〇だったら?」をお絵描きし、次々と波形を生成させます。
もう一例、8ワードのFIFOがオーバーフローしない、アンダーフローしないというプロパティを事前練習してみました。オーバーフロー波形はお絵描きで誘導して描かせています。Jasperは基本的に最短波形を見つけるので、デザインが存在しないこの状況でフェイル波形はいつもアンダーフローを“発見”するからです(アンダーフローは速やかに起こすことができ、オーバーフローするにはそれより時間が必要です)。オーバーフロー判定は、サイクル9でデータが8つ溜まり、サイクル10でさらにpushして、サイクル11でついにフェイルしています。多分、大丈夫そうですね。
そんなある日、ご質問が届きました。下記のプロパティ式をXcelium™シミュレータは受け付けるのにJasperは受け付けない (文法エラーする) というものでした。
信号SIG_AがHになり、次のサイクルからP_DELAYサイクル以内に信号SIG_Bが P_REPEAT回Hにならなかったら、そのサイクルでSIG_Cは真でなければならない
SIG_A |=>
(1'b1[*P_DELAY]) intersect (SIG_B[=P_REPEAT-1] or !SIG_B[*]) |->
SIG_C
原因は単にSystemVerilogバージョンの違いでした。Xceliumに合わせてJasperに「2012年版で解釈せよ」と指示することで (analyze -sv12) 読み込みエラーは解消しました。
ここで私が気になったのは、プロパティの元となった文章の切れの悪さです。「SIG_AがHにな」ったとき、なにが期待されているのかが一読して掴みにくかったのです。文章をもとに作ったプロパティ式もインプリケーション ( |=>, |-> ) が連なる、少し不安になるものでした。
文章を何度か読んでいるうち、SIG_Aがリクエスト的なもの、SIG_Bがそれに対する応答、SIG_Cは「ギブアップ」信号のように見えてきました。リクエストが届いたとき、所定回の応答が返されるのが第一に期待されていることであるが、叶わなかったときにはギブアップと言うべし、というルールのように思えたのです。第一の期待と第二の期待というのは、通常の論理ではor演算で表現することができます (例:P==1’b1 || Q==1’b1)。プロパティにもor演算子があります(元の式中でも使われていました)。この読み替えに従いプロパティを書き換えると次のようになりました。元の式よりはわかりやすくなっています(それでもintersectのような高難易度の演算子が使われていますが、そこはご容赦)。
信号SIG_AがHになったなら、次のいずれかが続くべし。1) P_DELAYサイクル以内にSIG_BがP_REPEAT回Hとなる 2) P_DELAYサイクル後にSIG_CがHとなる
SIG_A |=> ( 1’b1[*1:P_DELAY] intersect SIG_B[->P_REPEAT] ) // 第一の期待
or
( 1’b1[*P_DELAY-1] ##1 SIG_C ) // 第二の期待
さてここで、書き換え後のプロパティは書き換え前のものと果たして同じだろうかという疑問がわくことでしょう。特に書き換え前のものになんらか実績があるとき、書き換えて壊してしまうぐらいならそのままにしておこうという誘惑が首をもたげます。2つのプロパティが等しいか調べられたら――いわばアサーションどうしの等価性チェックです。これも、Jasper上で、ちょっとした操作で調べることができるのです。
assertとassumeは回路の正常動作を表現するものでした。つまり、この世のすべての波形を正常か異常かに分類します。
Jasperは、assumeがあれば必ずそれを守ります (異常と判定される波形を自動的に排除します)。またassertがあればそれをフェイルさせる波形を探し出します (どうしても波形が見つからないときにテストパスします)。2つのassert文のうち1つをassumeに転換しつつ他方のフェイル波形を探させることで、一方が正常と判定する波形を他方がどう判定するかがわかります。これを交互に行います。
2つのassert (ast_origとast_revと名付けました)をJasperに読み込ませ、GUI上の操作で一方をassumeに転換します。
証明を行うと、ast_origはパスしました。ast_revが正常と判定するすべての波形をast_origは正常と判定する、ということです。
先の図で表現すれば、こうですね。今のassume (ast_rev) の領域がassert (ast_orig) に完全に含まれる (同一またはより小さい) ということです。
次はassert/assumeを入れ替えて関係を調べます。再びマウス操作で立場を入れ替えた状況を作り証明すると、ast_revがフェイルしました。
書き換えにともないなんらか違いが発生したようです。2度の証明結果からJasperがこのように教えているので
- ast_revが正常と判定する波形をast_origは必ず正常と判定する
- ast_origが正常と判定する波形をast_revが異常と判定することがある
ast_origの方が判定が甘い (あるいはast_revが辛い) とわかります。下の分類で包含の関係です。
Case | プロパティ1 | プロパティ2 | 証明結果 | アサーションの関係 |
---|---|---|---|---|
1 | assume | assert | フェイル(CEX) | 食い違いもしくは完全相違 |
assert | assume | CEX | ||
2 | assume | assert | パス(Proven) | 包含、プロパティ1⊂プロパティ2 |
assert | assume | CEX | ||
3 | assume | assert | CEX | 包含、プロパティ2⊂プロパティ1 |
assert | assume | Proven | ||
4 | assume | assert | Proven | 同一 |
assert | assume | Proven |
ast_revのフェイル波形が、判定結果が分かれる波形です。式よりはわかりやすい・・・はずなので、見てみます。まずは波形を表示させ、アサーションの内容が際立つようQuiet 指定を適用しています。(Quiet:回路への入力においてHレベルを極力減らす指示)
SIG_AがHとなった後の12サイクル中でSIG_Bが一度だけHとなり、SIG_CはLのままです。これは、当初の文章に立ち返っても、アサーションがフェイルすべき波形のように思われます。ast_origのプロパティ式をよく見ると、P_DELAYサイクルの間に (1’b1[*P_DELAY] intersect ~) SIG_Bが、 P_REPEAT-1回HとなるかまったくHとならない (とき、最終的にSIG_CがHとなるべし)、と書かれていました。この式に従うならば、SIG_Bが1回Hとなった場合には、SIG_CはHとなる必要はありません。実はちょっとした不足がありました。文章を正しく表す式はSIG_Bの繰り返し回数に幅を持たせた
SIG_A |=>
(1'b1[*P_DELAY]) intersect (SIG_B[=1:P_REPEAT-1] or !SIG_B[*]) |->
SIG_C
でした。なお繰り返し演算子 [=n] ではゼロ回の繰り返しも指定できるので、もう少し簡単化してこのように書くこともできました。
SIG_A |=>
(1'b1[*P_DELAY]) intersect SIG_B[=0:P_REPEAT-1] |->
SIG_C
(でももう書き換えてしまったので、あまり気にしないでおきましょう)
ここまではプロパティ式どうしの比較を行いました。比較でなく式の意味を波形で観察するには、そう、先のwitnessカバー波形です。書き換え後のast_revのwitnessを表示させてみます。
witness1は第2の期待 (SIG_Bが不足し最後にSIG_CがHとなる)、witness2は第1の期待 (SIG_Bが所定回Hとなる) ですね、悪くはなさそうです。( Jasperがプロパティのor演算子を分解しています。witness1がcover ( SIG_A |-> (~ ##1 SIG_C) )、witness2が cover ( SIG_A |-> (~ intersect SIG_B[=P_REPEAT]) ) です)
本稿では、アサーション (+補助コード) を書いたプロパティファイルのみをJasperに与えて証明させるというアイデアをご紹介しました。Jasperが持つフィーチャを利用することで、アサーションが意味することを波形として見ることができ、そのアサーションをデザインに取り付ける前に、いわば「オフライン」でじっくりと検討・練習を行うことができます。ダイナミック検証、フォーマル検証、エミュレーションを問わず、ご活用ください。実際の操作をご覧になりたい方は、Jasper AEまでお声がけください。
フィールドエンジニアリング&サービス本部
システム&ベリフィケーション
水野 博之
Latest Issue
- OpenEyeのご紹介 人類の健康増進に貢献するために
- 組込みシステムの低コスト化、及び開発効率を向上させるDual-OS環境 ~Xtensaのセキュリティ拡張を用いた実現~
- ケイデンスオンラインサポート (Cadence Online Support: COS)のご紹介
- トピックス:CadenceLIVE Japan開催のご案内
- HiFi-TURB プロジェクト - AIおよび機械学習による乱流モデリング
- 「Celsius EC Solver」および「DataCenter Design Software and DataCenter Insight Platform」新機能のご紹介
- 新たな検証課題と高性能FastSPICEシミュレータSpectre FX
- PPA向上および短TAT化にも貢献! Digital Full Flowに融合したModus DFT Test Solutionのご紹介
- OrCAD 便利機能のご紹介
- AI/MLアプリケーションの普及に対応しつつ一段と高速化が進むDRAMメモリーインターフェース
- Chiplet接続 標準規格UCIeとCadence UCIe IPのご紹介
Archive
2023 Issues
2022 Issues
2021 Issues
2020 Issues