組み込みﾆｭｰｽ2002.4.17

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をｻﾎﾟｰﾄしたﾌﾟﾛﾊﾟﾃｨ･ﾁｪｯｷﾝｸﾞ･ﾂｰﾙの発表を予定しているという．

■連絡先
日本ｼﾉﾌﾟｼｽ株式会社
TEL:03-3346-7037