System Verilogアサーション・ハンドブック

評価：

System Verilogにおけるアサーションにまつわる言語機能の解説本。その昔、HDLの世界にはPSLというアサーション言語がありました。それはHDL記述に対して、実行時に満たすべき制約条件を記述できるものであり、それは常に満たすべき制約条件の他にある条件が整ってから一定時間後に別の条件が満たされなければならないといった時間の流れも含めた制約条件(時相論理)を記述する論理式言語でした。この言語のエッセンスはSystem Verilogに統合され、System Verilog Assertion(SVA)と言う言語機能となりました。このSVAについて解説しているのがこの本です。しかしそれだけではなく、SVAによる制約という論理式集合を用いて、HDL記述という論理式集合に対する制約条件を記述し、その条件の成立(統合した論理式集合に矛盾がない事)を形式的に確かめるという形式検証(あるいはFormal Method(だって、Formal Verificationっていうと納品する際に公式に提出する記録のための検証って意味に取られるんだもの))への繋がりまでが記述されています。assertionってソフトウェアにもありますよね。C言語のassertマクロとか。出発点はそこなのです。そこから始まり、ホーア論理(答えから計算を逆算して問題に辿り着くっていう計算の確かめ方、小学校で習ったでしょ?あれ+集合論)を経て、関数に対する事前条件、事後条件、不変条件の定義を行うというDesign By Contract(DBC)に繋がっていきましたよね。それをHDLで行った訳です。HDLの世界ではある信号(input)の立ち上がり/立下り(edge)とそれに因果関係がある信号(output)のedgeの関係が重要でしたから(それが要求であり、仕様なので)、それを確かめられるよう、時相論理が取り入れられました。そしてここまで厳密に記述された仕様と制約に対してこれらの制約条件を満たすか否かを数学的に証明できるかどうかという命題が与えられれば、形式検証に声が掛ってくるというわけです(今のところ普通はシミュレーションで確認ですけれど)。
さて、上位の要求から下位の要求へ(あるいは上位の設計仕様から下位の設計仕様と呼んだ方が誤解が無い?)要求が具体化される時、現実には具体化作業は二つに分かれ、出力が二つに分かれるのですと言ったら驚きますか?そしてその育った環境の異なる双子が等価であることを確かめる事こそが検証(V&VのVerification)であると言ったなら驚いてしまいますかね。
開発のフローにおいて要求は仕様に、仕様は実装に具体化されていきます。この流れにおいて行っていることは実は同じです。上位要求の行間を想像してより具体的に、より詳細に記述する。この為に決めなければいけない事について考察し、意見交換し、合意に至り、上位要求に対して、100%満たしている事、無理な意味論的解釈が行われていない事を確認して、より具体的に記述する。これが、設計の流れです。検証でも同じことが行われます。上位要求の行間を想像してより具体的に、対象の振舞い/形を想像して、より具体的にその型を決めます。それがテストケースであり、テストシナリオであり、テストパターンとなり現れます。つまり、同じ上位要求から二つの異なる解釈書を作り、それが同じであることを確かめているのです。上位要求から下位要求への具体化のステップ数はこだわりの対象ではありません。意味が通じる程度の具体化の繋がりの連続で、コピーを作れば同じものが作れるというレベルの抽象度の設計情報に至れれば良いのです。これがデザインツリー(デザイン木)です。
であれば、全く相互にコミュニケーションしていない2つの設計/実装の等価性を確かめる事も実は検証の意味を成しているのではないかと思います。
まぁ、そんなことはさておいて、LSIの設計において設計の正しさを確認する作業は必須です。その際、HDLでモニタを記述する事も出来ますし、対抗するgolden modelとの等価性を検証することもできますし(有れば)、検証結果の目視確認でデータシートの内容との等価性を確認する事も出来ますけれど、その際の合理的な手段の一つとして、SVAは存在するのだと思います(言語の記述の統一性についてはちょっと物申したいですが・・・)。HDLで設計を行い、そのRTLモデルの検証を行わなくてはならなくなったが、何か良い方法は無いものだろうかという人にお勧めです。この手の本は読んでおくと仕様記述時の表現方法にも影響を与えてくるので油断なりませんよ? >> 続きを読む

2012/12/16 by Shimada

「System Verilogアサーション・ハンドブック」のレビュー