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