ソースを表示

出典: くみこみックス

以下に示された理由により ページの編集 を行うことができません:

以下にソースを表示しています:

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

フォーマル・ベリファイア に戻る。