フォーマル・ベリファイア
出典: くみこみックス
版間での差分
M (1 版) |
|||
7 行 | 7 行 | ||
<br> | <br> | ||
【出典】西久保 靖彦;基本システムLSI用語辞典,CQ出版社,2000年5月. | 【出典】西久保 靖彦;基本システムLSI用語辞典,CQ出版社,2000年5月. | ||
- | + | <!-- 【著作権者】西久保 靖彦氏 --> | |
<br> | <br> | ||
<br> | <br> |
2009年3月13日 (金) 07:40の版
フォーマル・ベリファイア【Formal Verifier】
設計データを数学的に解析することによって,論理機能を検証するツール.フォーマル・ベリファイアには二つのタイプがある.一方は,二つの設計データの論理機能が等価であるかどうかを調べる等価性検証ツール.もう一方は,設計された論理回路が,特定の設計仕様(プロパティ)を満たしているかどうかを調べるプロパティ検証(プロパティ・チェッキング,モデル・チェッキング)ツールである.
フォーマル・ベリファイアのうち,等価性検証ツールは実用段階に入っている.等価性検証ツールを利用する場合,論理機能的に正しいことが保証されている参照データを用意する必要がある.参照データが論理機能的に正しいかどうかは,事前に論理シミュレータなどで確認しておく.フォーマル・ベリファイアの内部処理には,二分決定グラフ(BDD:Binary Decision Diagram)を使うことが多い.
【出典】西久保 靖彦;基本システムLSI用語辞典,CQ出版社,2000年5月.