フォーマル・べリファイアフォーマル・べリファイア（formal verifier）は，設計結果の回路を数学的に解析することで，その結果を検証するツール。シミュレータのように設計結果の回路を疑似的に動作させて検証するのではなく，設計結果そのものを解析する。この意味では，スタティック・タイミング・アナライザもフォーマル・ベリファイアの仲間といえる。 ただし，現在EDAの世界で，フォーマル・ベリファイアといえば，論理機能を検証するために，設計結果そのものを数学的に解析するツールを指している。フォーマル・ベリファイアの一番のメリットは，その定義にあるように，シミュレーション・パターンが必要ない点である。作成する手間が省けるうえ，検証に漏れがない。しかし，後述するようにどんな場合でも有効というわけではない。 2つの種類がある 現在，フォーマル・ベリファイアと呼ばれている市販ツールは2種類ある。仕様検証（property c
Synopsys - Wikipedia
