Synopsys，検証言語OpenVeraにIntel社開発のプロパティ検証用記述を追加

　米国Synopsys社は，同社が公開している検証言語OpenVeraをバージョン・アップした．今回のOpenVera 2.0では，プロパティ・チェッキング・ツールやアサーション・チェッカなどで利用できるアサーション表現を追加した．Intel社が社内で利用している内製検証言語ForSpecのアサーション表現をOpenVeraに取り込んだ．

　プロパティ・チェッキング・ツールとはフォーマル・ベリフィケーション（形式的検証）ツールの一種で，設計したディジタル回路が与えられた命題（プロパティ）を満足するかどうかを数学的に証明するツールである．例えば，「出力Aは絶対に‘0’にならない」というプロパティを与えると，回路を数学的にチェックして真か偽かを返す．また，出力信号が‘0’になる場合は，どういう条件でそれが起こるかということも示す．アサーション・チェッカとは，シミュレーションが実行されている間，与えられた命題（アサーション）が遵守されているかをモニタするチェッカ・モジュールである．前者は静的な検証であり，後者は動的な検証である．また，ここでの命題は，時間の概念を含む「時間論理（時相論理）」の命題になる．

　プロパティ・チェッキング・ツールとアサーション・チェッカは出自のまったく異なるEDA技術であり，これまで記述表現が統一されていなかった．OpenVera 2.0ではこれを共通にした．OpenVera 2.0のLRM（language reference manual）は，OpenVeraのWebサイトからダウンロードできる．

　さらに同社は，OpenVeraに準拠した9種類の検証用IPが出荷されたこと，新たに3社のEDAツールがOpenVeraのサポートを開始したこと，オンラインのディスカッション・フォーラムを発足したこと，新たに11社がOpenVeraに関する企業コンソーシアムであるCatalystプログラムに参加したことを発表し，OpenVeraの勢いを誇示した．

　Synopsys社では，近々にOpenVera 2.0をサポートしたプロパティ・チェッキング・ツールの発表を予定しているという．