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