検証
自己検証型テストベンチとcocotbから、UVM、SymbiYosysによる形式検証、CIでのVerilatorまで、FPGA設計が意図どおりに動くことをシリコンに載せる前に証明する方法を解説します。
概要
検証とは、設計が仕様を満たしていることを、作る前に示す作業です。FPGAではデバイスを再プログラムできるため、間違いのコストはASICより低いものの、ゼロには程遠いです。ボード上で見つかったバグはオンチップロジックアナライザで切り分けるのに何日もかかることがあり、現場で見つかったバグは製品リコールにつながることもあります。このハブは、単一モジュールからシステムまでスケールする検証手法を求めるエンジニアと、これまで「波形を眺める」ことしかしておらず、それでは足りないと感じ始めたすべての方のためのものです。
その幅は、数個のベクトルを駆動するだけの直接指定テストベンチから、カバレッジ付きの制約付きランダムシミュレーション、あらゆる入力をカバーする形式的証明にまで及びます。ほとんどのプロジェクトには組み合わせが必要です。選択は、設計が間違っていた場合にどれだけのコストがかかるかによります。
重要な考え方
自己検証型テストベンチ
テストベンチとは、検証対象（DUT）をインスタンス化し、その入力を駆動し、出力を観測する合成不可能なHDL（またはPython、C++）です。波形を眺めることに対する最初の改善は、自己検証型にすることです。テストベンチが出力の期待値を計算して比較し、合格か不合格かを表示します。2つ目の改善は役割を分離することです。ドライバはトランザクションをピンの動きに変換し、モニタはピンの動きをトランザクションに戻し、スコアボードはそれをリファレンスモデルと比較し、テスト自体はどのトランザクションを送るかを選ぶだけにします。この構造こそUVMが形式化したものですが、どんな規模でも有用であり、素のVHDL、SystemVerilog、Pythonでも構築できます。
cocotb、UVM、制約付きランダム
cocotbを使うと、テストベンチをPythonで書き、無償のIcarus Verilog、GHDL、Verilatorを含む主要なあらゆるシミュレータに対して実行できます。コルーチンがクロックエッジを待ち、リファレンスモデルにはPythonエコシステム全体が使え、DUTはHDLのままです。オープンソースコアや小規模チームではデフォルトになっています。
UVM（Universal Verification Methodology）は、AccelleraとIEEEが標準化したSystemVerilogのクラスライブラリです。大規模なASICチームが使うエージェント、シーケンス、スコアボード、ファクトリの構造を定義しています。その強みは再利用性と制約付きランダム生成です。制約で正当な入力空間を記述し、シミュレータに何千ものランダムケースを選ばせ、機能カバレッジで空間のどの部分がヒットしたかを確認します。代償は急な学習曲線と、商用シミュレータの必要性です。無償ツールはUVMが必要とするSystemVerilogのクラス機能を完全にはサポートしていないからです。FPGAプロジェクトでは、IPベンダーの世界では一般的で、小規模チームではまれです。VHDLユーザーには、OSVVMとUVVMがSystemVerilogなしで同様の考え方を提供します。
形式検証
形式検証ツールはシミュレーションを行いません。設計を方程式の集合として扱い、あるプロパティが違反され得るかどうかをソルバーに問います。有界モデル検査は、Nサイクル以内に反例が存在しないことを証明します。帰納法はそれをすべてのサイクルについて証明します。プロパティはSystemVerilogアサーションまたはPSLとして書かれ、同じアサーションはシミュレーションでも実行できます。YosysHQのSymbiYosys（SBY）はオープンソースのソルバーを駆動し、Verilogで無償で使えます。AMD Vivado、Siemens Questa、Cadence JasperGoldがベンダーの形式検証を提供します。形式検証は、FIFO、アービタ、バスプロトコル準拠、そしてランダムシミュレーションでは何年かかっても当たらないようなまれなイベント順序にバグが潜むあらゆるものに対して、比類のない力を発揮します。大きな算術演算や深いパイプラインは苦手です。
Verilator、カバレッジ、CI
Verilatorは合成可能なSystemVerilogをC++モデルにコンパイルし、イベント駆動シミュレータの10倍から100倍の速さで実行します。ソフトコアでLinuxをブートするといった、ソフトウェア駆動の長いテストに適したツールであり、ラインカバレッジとトグルカバレッジを報告します。シミュレーションを継続的インテグレーションに組み込むということは、コミットのたびにVerilator、Icarus、GHDL、あるいはライセンスされたシミュレータを使ったコンテナでテストスイートが実行され、失敗すればマージがブロックされるということです。CIのないハードウェアプロジェクトは、誰かがテストの再実行を覚えていることに頼っています。
どこから始めるか
- /learn/beginner/06-simulation-and-testbenches/は、最初の自己検証型テストベンチを書きます。
- /learn/beginner/07-finite-state-machines/と/learn/beginner/09-memories-block-ram-and-fifos/には、バグが隅に隠れる設計のためのテストベンチが含まれています。
cocotb、SystemVerilogアサーション、SymbiYosysによる最初の形式的証明に関する中級レッスンは準備中です。
ツールとベンダー
| ツール | 種類 | 言語 | 費用 | 典型的な用途 |
|---|---|---|---|---|
| Icarus Verilog | イベントシミュレータ | Verilog、一部SV | 無償 | 小規模なVerilog設計、cocotb |
| GHDL | イベントシミュレータ | VHDL | 無償 | VHDL設計、cocotb、Yosys経由の形式検証 |
| Verilator | コンパイル型シミュレータ | SystemVerilog | 無償 | 高速なシステムレベルテスト、CI |
| cocotb | テストベンチフレームワーク | Python | 無償 | 上下いずれのシミュレータでも |
| SymbiYosys | 形式検証 | Verilog、SVA | 無償 | モジュール単位の証明 |
| Vivado Simulator | イベントシミュレータ | VHDL、Verilog、SV | Vivadoに付属、無償 | AMD IPのシミュレーション |
| Questa、Xcelium、VCS | イベントシミュレータ | すべて、完全なUVM | 商用 | UVM、大規模な混合言語プロジェクト |
| OSVVM、UVVM | VHDLライブラリ | VHDL | 無償 | VHDLでの制約付きランダムとカバレッジ |
ベンダーのシミュレータは/vendors/amd/、/vendors/altera/、/vendors/opensource/で説明しています。
よくある間違い
- 波形ビューアで目視確認して、テスト済みと呼ぶ。
- 設計そのものをリファレンスモデルに使う。コードがコードと等しいことしか証明できません。
- 比較に到達しないせいで、DUTがどうであれ合格してしまうテストを書く。
- DUTがサンプリングするのと同じエッジで入力を駆動し、バグを隠したり捏造したりする競合状態を作る。
- ラインカバレッジ100%を、振る舞いの100%を実行したかのように報告する。
- CIからシミュレーションを外し、設計の変更とともにテストスイートが腐っていく。
さらに深く
- cocotb documentation: インストール、コルーチンモデル、シミュレータのサポート状況。
- Verilator user guide: コンパイル済みモデルのビルドと実行。
- SymbiYosys documentation: 形式検証フロー、ソルバー、プロパティ言語のサブセット。
- Accellera UVM standard page: クラスライブラリのリファレンスとユーザーガイド。
- OSVVM: VHDL向け検証ライブラリ。
- IEEE 1800-2023, SystemVerilog: アサーション、カバレッジ、UVMが依存するクラス機能を定義しています。