フォーマル・ベリファイア

出典: くみこみックス

版間での差分
最新版 (2009年3月13日 (金) 07:50) (ソースを表示)
M (1 版)
 

最新版

フォーマル・ベリファイア【Formal Verifier】

 設計データを数学的に解析することによって,論理機能を検証するツール.フォーマル・ベリファイアには二つのタイプがある.一方は,二つの設計データの論理機能が等価であるかどうかを調べる等価性検証ツール.もう一方は,設計された論理回路が,特定の設計仕様(プロパティ)を満たしているかどうかを調べるプロパティ検証(プロパティ・チェッキング,モデル・チェッキング)ツールである.  フォーマル・ベリファイアのうち,等価性検証ツールは実用段階に入っている.等価性検証ツールを利用する場合,論理機能的に正しいことが保証されている参照データを用意する必要がある.参照データが論理機能的に正しいかどうかは,事前に論理シミュレータなどで確認しておく.フォーマル・ベリファイアの内部処理には,二分決定グラフ(BDD:Binary Decision Diagram)を使うことが多い.

【出典】西久保 靖彦;基本システムLSI用語辞典,CQ出版社,2000年5月.

関連項目

表示