(57)【要約】【課題】プロパティ言語で生成されたプロパティ記述から仕様書を逆生成し、逆生成した仕様書と元の仕様書とを比較してプロパティ記述のミスを訂正する検証支援装置等を提供する。【解決手段】ハードウェアの検証を支援する検証支援装置１であって、プロパティ言語または検証ライブラリで記載されたプロパティ記述４０２を入力するプロパティ記述入力部４７０と、前記入力されたプロパティ記述４０２を解析するプロパティ解析処理部４１０と、該プロパティ解析部４１０が解析した結果に基づいて所定の形式の仕様書を生成する仕様書逆生成部４２０とを備えることを特徴とする。【選択図】図４
2009086918.tif 000002
【特許請求の範囲】
【請求項１】
ハードウェアの検証を支援する検証支援装置であって、
プロパティ言語または検証ライブラリで記載されたプロパティ記述を入力する入力部と、
前記入力されたプロパティ記述を解析するプロパティ解析部と、
該プロパティ解析部が解析した結果に基づいて所定の形式の仕様書を生成する仕様書逆生成部とを備えることを特徴とする、検証支援装置。
【請求項２】
第１の仕様書に基づいて作成されたプロパティ記述を用いた、ハードウェアの検証を支援する検証支援装置であって、
プロパティ言語または検証ライブラリで記載されたプロパティ記述を入力する入力部と、
前記入力されたプロパティ記述を解析するプロパティ解析部と、
前記プロパティ解析部が解析した結果に基づいて、前記第１の仕様書と同じ形式で第２の仕様書を生成する仕様書逆生成部とを備えることを特徴とする、検証支援装置。
【請求項３】
請求項２に記載の検証支援装置において、
更に、前記第１の仕様書を電子データとして読み込む仕様書入力部と、
前記仕様書逆生成部が生成した第２の仕様書及び前記第１の仕様書を比較し、相違する箇所及び／または一致する箇所を検出する仕様書比較部を備えることを特徴とする、検証支援装置。
【請求項４】
請求項３に記載の検証支援装置において、
前記仕様書比較部が比較した結果、前記第１の仕様書及び第２の仕様書の相違する箇所が検出された場合に、当該相違する箇所に対応する前記プロパティ記述における該当する箇所を、前記第１の仕様書の記載に基づいて修正するプロパティ記述修正部を備えることを特徴とする、検証支援装置。
【請求項５】
請求項２ないし請求項４のいずれかに記載の検証支援装置において、
前記第１と第２の仕様書は、少なくとも入力条件及び出力条件がテストケース毎に記載されており、
前記仕様書逆生成部が生成した第２の仕様書の入力条件について、当該入力条件が同一である複数のテストケースがある場合に、当該複数のテストケースを同一のテストケースとして併合する併合部を備え、
前記併合部が併合した結果に基づいて、前記プロパティ記述を修正することを特徴とする、検証支援装置。
【請求項６】
入力部とプロパティ解析部と仕様書逆生成部とを有するコンピュータを用いて、ハードウェアの検証を支援する検証支援方法において、
前記入力部を用いて、プロパティ言語または検証ライブラリで記載されたプロパティ記述を入力する入力ステップと、
前記プロパティ解析部を用いて、前記入力されたプロパティ記述を解析するプロパティ解析ステップと、
前記仕様書逆生成部を用いて、前記プロパティ解析ステップにて解析された結果に基づいて、所定の形式で仕様書を生成する仕様書逆生成ステップとを含む検証支援方法。
【請求項７】
ハードウェアの検証を支援するように、入力部とプロパティ解析部と仕様書逆生成部とを有するコンピュータを実行させるための検証支援プログラムにおいて、
前記入力部を用いて、プロパティ言語または検証ライブラリで記載されたプロパティ記述を入力する入力手順と、
前記プロパティ解析部を用いて、前記入力されたプロパティ記述を解析するプロパティ解析手順と、
前記プロパティ解析手順が解析した結果に基づいて、前記第１の仕様書と同じ形式で第２の仕様書を生成する仕様書逆生成手順とをコンピュータに実行させるための検証支援プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、電子機器等に搭載されるハードウェアの検証を支援する検証支援装置に関し、特に、プロパティ言語や検証ライブラリで作成されたプロパティ記述から仕様書を生成して、ハードウェアの検証を支援する検証支援装置等に関する。
【背景技術】
【０００２】
電子機器に搭載されるＬＳＩ、ＡＳＩＣ、ＦＰＧＡ等のハードウェア開発では、全体工程のうち検証にかかる期間が約７割を占めると言われており、製品の市場投入時期に大きく影響する。通常、ハードウェアの検証を行う場合、検証者はテストベンチを作成し、回路情報（一般的にＲｅｇｉｓｔｅｒ  Ｔｒａｎｓｆｅｒ  Ｌｅｖｅｌを略してＲＴＬと呼ばれている）に対してテストパターンを与え、期待した結果が出力されるかどうかを確認する。近年、製品に求められる機能は複雑化および多機能化しており、それに伴い検証も困難になってきている。特にテストベンチやテストパターンの作成、結果確認作業に要する時間とコストは膨大なものとなっている。
【０００３】
このような課題に対して、各電機メーカーや研究機関、大学等ではハードウェアの検証技術に対する様々な研究が進められており、中でもプロパティを用いたアサーション・ベース検証が一般的になりつつある。プロパティとは開発対象の機能や構造の特徴（仕様）であり、例えば、「条件Ｘが成立したとき、常に結果はＹである」というような形式で表現される。プロパティは論理シミュレータや形式的検証ツール等の検証装置が解釈できるように、ＰＳＬやＳｙｓｔｅｍＶｅｒｉｌｏｇ  Ａｓｓｅｒｔｉｏｎに代表されるプロパティ言語や検証ライブラリであるＯＶＬ（Ｏｐｅｎ  Ｖｅｒｉｆｉｃａｔｉｏｎ  Ｌｉｂｒａｒｙ）で記述され、ＨＤＬ（Ｈａｒｄｗａｒｅ  Ｄｅｓｃｒｉｐｔｉｏｎ  Ｌａｎｇｕａｇｅ）で記述される回路情報とは表現方法が異なる。アサーション・ベース検証において、検証装置は回路情報に違反がないかをプロパティ記述に基づいて検査し、違反があれば検証者に警告を与える。アサーション・ベース検証では違反がいつ、どこで発生したのかを特定しやすいため、タイミング確認や違反箇所の修正が従来よりも正確かつ容易になり、検証期間を大幅に短縮することができる。
【０００４】
また、アサーション・ベース検証に関する技術として、特許文献１に示す技術がある。特許文献１に示す技術は、アサーション・ベース検証において、検証者によるアサーション記述言語仕様の修得を不要にし、人為的なミスを軽減してテスト精度の向上を図る技術であり、デザイン仕様書等の設計資料を入力し、デザイン仕様書等の設計資料から入出力記述子および論理条件データを取得し、入出力記述子に論理条件を付加して入出力論理条件ファイルを生成する手段と、別途入力されるアサーション記述言語仕様指定によりアサーション記述言語仕様を選択する手段と、選択された言語仕様に基づき前記入出力論理条件ファイルをアサーション記述に変換する変換部と、変換されたアサーション記述をテキスト形式のファイルとして出力する手段とを備えたアサーション記述自動生成装置を用い、アサーション記述を人手でよらず自動生成できるようにする技術である。
【特許文献１】特開２００７−１１４６７号公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
アサーション・ベース検証において、仕様書とプロパティの記述が論理的に等価である必要がある。つまり「正しいプロパティ記述」でなければならない。しかし、現状は、プロパティ記述の作成は、仕様書を参照しながらマニュアルで行うことが多く、作成過程において記述ミスが混入する可能性が非常に高い。ミスが混入してしまったプロパティで検証を行うと回路情報を正しく検証することができず、検証機関の遅れや品質の低下を招く要因となり、むしろ逆効果となってしまう。
【０００６】
ミスの混入を防止するため検証者や第三者によるプロパティ記述に対する目視レビューの実施が考えられる。しかし、レビューを行う人間がプロパティ言語に精通していない場合は、プロパティ記述の理解が難しく、またプロパティ記述の数が多ければ、すべてのミスを発見することは容易ではない。このようにプロパティ記述が仕様書と等価であることを証明するのは極めて困難であり、アサーション・ベース検証の課題となっている。
【０００７】
特許文献１の技術を利用した場合は、設計資料に基づいてアサーション記述を自動で生成するため、処理の手間は省くことができるが、生成されたアサーション記述が正確かどうかを検証するには、上記のような目視レビューが必要となり、仕様書とアサーション記述が等価であるかどうかを証明するのは困難となってしまう。
【０００８】
そこで、本発明は前記課題を解決するためになされたものであり、プロパティ言語で生成されたプロパティ記述から仕様書を逆生成し、逆生成した仕様書と元の仕様書とを比較してプロパティ記述のミスを訂正する検証支援装置、検証支援方法、及び、検証支援プログラムを提供することを目的とする。
【課題を解決するための手段】
【０００９】
（１．仕様書の逆生成処理）
本発明に係る検証支援装置は、ハードウェアの検証を支援する検証支援装置であって、プロパティ言語または検証ライブラリで記載されたプロパティ記述を入力する入力部と、前記入力されたプロパティ記述を解析するプロパティ解析部と、該プロパティ解析手段が解析した結果に基づいて所定の形式の仕様書を生成する仕様書逆生成部とを備えることを特徴とする。
【００１０】
このように、本発明においては、プロパティ言語で記載されたプロパティ記述を解析し、その結果に基づいて仕様書を逆生成するため、プロパティ言語に精通していない人であっても、仕様書の形式でプロパティ記述の内容を理解して確認することができるという効果を有する。
【００１１】
（２．予め作成された仕様書と同形式の仕様書の逆生成処理）
本発明に係る検証支援装置は、第１の仕様書に基づいて作成されたプロパティ記述を用いた、ハードウェアの検証を支援する検証支援装置であって、プロパティ言語または検証ライブラリで記載されたプロパティ記述を入力する入力部と、前記入力されたプロパティ記述を解析するプロパティ解析部と、前記プロパティ解析部が解析した結果に基づいて、前記第１の仕様書と同じ形式で第２の仕様書を生成する仕様書逆生成部とを備えることを特徴とする。
【００１２】
このように、本発明においては、プロパティ言語で記載されたプロパティ記述を解析し、その結果に基づいて仕様書を逆生成するため、プロパティ言語に精通していない人であっても、仕様書の形式でプロパティ記述の内容を理解して確認することができるという効果を有すると共に、プロパティ言語に精通している人であっても、プロパティ言語を解読するよりも仕様書としてプロパティ記述を確認するほうがレビュー等の作業を行いやすく、第１の仕様書と同じ形式で第２の仕様書が生成されるため、検証作業を効率的に行うことができるという効果を有する。
なお、プロパティ言語は、ＰＳＬやＳｙｓｔｅｍＶｅｒｉｌｏｇ  Ａｓｓｅｒｔｉｏｎ等、いかなる言語であってもよい。
【００１３】
（３．仕様書の比較処理）
本発明に係る検証支援装置は、更に、前記第１の仕様書を電子データとして読み込む仕様書入力部と、前記仕様書逆生成部が生成した第２の仕様書及び前記第１の仕様書を比較し、相違する箇所及び／または一致する箇所を検出する仕様書比較部を備えることを特徴とする。
【００１４】
このように、本発明においては、仕様書逆生成手段がプロパティ記述に基づいて生成した第２の仕様書と電子データとして読み込まれた第１の仕様書とを比較して、相違する箇所及び／または一致する箇所を検出するため、第１の仕様書とプロパティ記述の等価性を間接的に、瞬時に証明することができるという効果を有する。
【００１５】
（４．プロパティ記述の修正処理）
本発明に係る検証支援装置は、前記仕様書比較部が比較した結果、前記第１の仕様書及び第２の仕様書の相違する箇所が検出された場合に、当該相違する箇所に対応する前記プロパティ記述における該当する箇所を、前記第１の仕様書の記載に基づいて修正するプロパティ記述修正部を備えることを特徴とする。
【００１６】
このように、本発明においては、仕様書逆生成手段がプロパティ記述に基づいて生成した第２の仕様書と第１の仕様書との相違する箇所が検出された場合に、その相違する箇所に該当するプロパティ記述の記載を、第１の仕様書に基づいて修正するため、第１の仕様書と論理的に等価なプロパティ記述を得ることができるという効果を有する。
【００１７】
また、プロパティ記述修正部により修正されたプロパティ記述を用いて、検証作業を行うことで、検証者が回路情報を正しく検証することができ、結果的にアサーション・ベース検証の長所を最大限に活用して検証期間の大幅な短縮が可能になるという効果を有する。
さらに、装置がプロパティ記述の修正を自動で行うことで、検証作業を効率的に行うことができる。
【００１８】
（５．テストケースの併合処理）
本発明に係る検証支援装置は、前記第１と第２の仕様書は、少なくとも入力条件及び出力条件がテストケース毎に記載されており、前記仕様書逆生成部が生成した第２の仕様書の入力条件について、当該入力条件が同一である複数のテストケースがある場合に、当該複数のテストケースを同一のテストケースとして併合する併合部を備え、前記併合部が併合した結果に基づいて、前記プロパティ記述を修正することを特徴とする。
【００１９】
このように、本発明においては、仕様書逆生成部がプロパティ記述に基づいて生成した第２の仕様書について、入力条件が同一であるテストケースが複数ある場合に、当該複数のテストケースを同一のテストケースとして併合するため、例えば、第１の仕様書には、１つのテストケースとして記載されているが、プロパティ記述では複数のテストケースに分かれているような場合であっても、それらを併合して１つのテストケースとして取り扱うことができ、第１の仕様書の内容に自動で合致させることができるという効果を有する。つまり、第１の仕様書と、その仕様書に基づいて生成されたプロパティ記述（例えば、プログラマにより生成されたプロパティ記述）は、内容的には同一であっても、異なる表現で記載される場合がある。このような場合、第１の仕様書とプロパティ記述は実質的には同一である。本発明は、表現が異なっている場合であっても、内容が実質的に同一である場合には、第１の仕様書とプロパティ記述は等価であると判断することができる。
【００２０】
なお、併合手段が併合した結果に基づいて、プロパティ記述の修正を行うようにしているが、プロパティ記述の修正ではなく、第２の仕様書を修正するようにしてもよい。この場合、再度仕様書比較部により仕様書の比較を行い、元の仕様書と相違する箇所があればプロパティ記述を修正するようにしてもよい。
【００２１】
また、併合手段が併合した結果に基づいてプロパティ記述の修正を行う場合は、その修正されたプロパティ記述から、再度仕様書逆生成部により仕様書の逆生成を行い、仕様書比較部により仕様書の比較を行って、相違する箇所があればプロパティ記述を修正するようにしてもよい。
【００２２】
これまで、本発明を装置として示したが、所謂当業者であれば明らかであるように本発明をシステム、方法、及び、プログラムとして捉えることもできる。これら前記の発明の概要は、本発明に必須となる特徴を列挙したものではなく、これら複数の特徴のサブコンビネーションも発明となり得る。
【発明を実施するための最良の形態】
【００２３】
以下、本発明の実施の形態を説明する。本発明は多くの異なる形態で実施可能である。従って、本実施形態の記載内容のみで本発明を解釈すべきではない。また、本実施形態の全体を通して同じ要素には同じ符号を付けている。
【００２４】
本実施の形態では、主に装置について説明するが、所謂当業者であれば明らかな通り、本発明はシステム、方法、及び、コンピュータを動作させるためのプログラムとしても実施できる。また、本発明はハードウェア、ソフトウェア、または、ハードウェア及びソフトウェアの実施形態で実施可能である。プログラムは、ハードディスク、ＣＤ−ＲＯＭ、ＤＶＤ−ＲＯＭ、光記憶装置、または、磁気記憶装置等の任意のコンピュータ可読媒体に記録できる。さらに、プログラムはネットワークを介した他のコンピュータに記録することができる。
【００２５】
（本発明の第１の実施形態）
（１．概要）
以下に、本実施形態に係る検証支援装置の概要を説明する。図１は、本実施形態における設計者が作成した仕様書と検証対象となるハードウェアの一例である。図１（ａ）の設計者が作成した仕様書は、図１（ｂ）のハードウェアに関する入力条件（値）と出力条件（値）を表している。項の列に記述している１〜４の番号は説明を簡単にするために記載しているが、実際はなくてもよい。検証者は図１（ａ）の仕様書からプロパティを抽出する。すなわち、項１は「入力Ａが０かつ入力Ｂが０ならば、出力Ｃは常に０」、項２は「入力Ａが０かつ入力Ｂが１ならば、出力Ｃは常に１」というプロパティを抽出する。項３、４についても同様である。
【００２６】
なお、本実施形態では、仕様書がパーソナルコンピュータ等で電子データとして作成されていることを前提にしている。仕様書が手書きの仕様書である場合は、既存のＯＣＲ（Ｏｐｔｉｃａｌ  Ｃｈａｒａｃｔｅｒ  Ｒｅａｄｅｒ）を用いた表データの読み込み技術を適用すればよいので、ここでは説明を省略する。
【００２７】
次に、抽出したプロパティに基づき、プロパティ言語を用いてプロパティ記述に翻訳する。図２は図１（ａ）から抽出したプロパティをプロパティ言語の１つであるＰＳＬを用いてプロパティ記述に変換したものである。なお、項番１〜４は、ＰＳＬとは関係なく、説明のために記述している。
【００２８】
図２の項１において、ａｓｓｅｒｔ＿1は、プロパティ記述に付与された任意の名前である。次のａｓｓｅｒｔはＰＳＬの予約語であり、これ以降の条件式についてハードウェアに違反があれば検証装置からメッセージを出力することを意味する。ａｌｗａｙｓ（｛Ａ＝０  ａｎｄ  Ｂ＝０｝｜−＞｛Ｃ＝０｝）は条件式であり図１（ｂ）のハードウェアにおいて、「入力Ａが０かつ入力Ｂが０の条件のとき、出力Ｃが常に０」であることを表しており、図１（ａ）に示した項１のプロパティと一致する。条件式の中の記号｜−＞はＰＳＬの予約語であり、｜−＞の左辺の条件が成立したとき、右辺の条件が成立するという原因と結果を表している。以降の項２〜項４も同じである。
【００２９】
ただし、この例では図１（ａ）の項４のプロパティ翻訳過程においてミスが発生しており、図２の項４は間違ったプロパティ記述となっている。図２の項４の正しいプロパティ記述はａｓｓｅｒｔ  ａｌｗａｙｓ（｛Ａ＝１  ａｎｄ  Ｂ＝１｝｜−＞｛Ｃ＝３｝）でなければならない。
【００３０】
この間違ったプロパティ記述を用いてハードウェアの回路情報を検証した場合、検証装置は、たとえ回路情報が正しくても違反メッセージを出力する。これに対し、検証者は回路情報とプロパティ記述のどちらが間違っているのかを特定しなれければならず、両者を見直すことになる。結果として従来以上に時間を費やしてしまう。
【００３１】
このように回路情報とプロパティ記述のどちらが間違っているか特定しなければならない場合に、本実施形態に係る検証支援装置は、プロパティ記述を解析して仕様書を逆生成する。その逆生成した仕様書と、設計者が作成した仕様書を比較して、相違する箇所があれば、プロパティ記述に間違いがある可能性が非常に高い。また、相違する箇所がない場合は、回路情報が間違っている（仕様書通りではない）と判断することができる。そして、プロパティ記述に間違いがあると判断した場合は、間違っていると思われる箇所を、設計者が作成した仕様書に合わせて修正する。そうすることで、プロパティ記述が仕様書を等価となり、検証作業を正確に行うことができる。
【００３２】
仕様書を逆生成することで、プロパティ言語に精通していない人でもプロパティ記述の内容を理解して把握することができると共に、逆生成する元となるプロパティ記述は、所定のルール（例えば、ＰＳＬであればＰＳＬのプログラミングルール）に基づいて形式的に作成されているため、コンピュータにとっては解析を行いやすく、正確な解析が可能となり、確実に仕様書を逆生成することができる。
【００３３】
一方、プロパティ記述を作成する際に、プログラマが仕様書を参照しながらマニュアルで行う場合は、作成過程でミスが混入してしまう可能性がある。また、プロパティ記述を自動で作成する場合は、設計者が仕様書を作成する際の作成ルールを細かく設定し、その設定通りに仕様書が作成されていなければ、正確なプロパティ記述を生成することはできない。つまり、いずれの場合も、プロパティ記述と設計者が作成した仕様書が完全に等価であるとは限らない。従って、本発明のように、設計者が作成した仕様書からプロパティ記述を作成する過程と異なる過程（異なるアルゴリズム）でプロパティ記述から仕様書を逆生成して、設計者の仕様書との相違箇所を検出することは、作業の効率性においても、正確性においても非常に有効な手段となる。
【００３４】
（２．構成と機能）
（２−１  検証支援装置のハードウェア構成）
図３は、本実施形態に係る検証支援装置のハードウェアの構成図である。検証支援装置１は、ＣＰＵ(Central  Processing  Unit)３０１、ＲＡＭ(Random  Access  Memory)３０２、ＲＯＭ(Read  Only  Memory)３０３、フラッシュメモリ(Flash  memory)３０４、外部記憶装置であるＨＤ(Hard  disk)３０５、ＬＡＮ(Local  Area  Network)カード３０６、マウス３０７、キーボード３０８、ビデオカード３０９、このビデオカード３０９と電気的に接続する表示装置であるディスプレイ３０９ａ、サウンドカード３１０、このサウンドカード３１０と電気的に接続する音出力装置であるスピーカ３１０ａ及びフレキシブルディスク、ＣＤ−ＲＯＭ、ＤＶＤ−ＲＯＭ等の記憶媒体を読み書きするドライブ３１１からなる。
なお、上記ハードウェア構成はあくまで一例を示したものであり、構成要素の変更をすることができるのは当然である。
【００３５】
（２−２  検証支援装置のモジュール構成と機能）
図４は、本実施形態に係る検証支援装置１のモジュール構成図である。検証支援装置１は、プロパティ記述入力部４７０と、プロパティ言語情報データベース４０５と、プロパティ解析処理部４１０と、仕様書逆生成処理部４２０と、比較情報データベース４２５と、仕様書入力部４７１と、仕様書比較処理部４３０と、修正情報データベース４４０と、プロパティ記述修正処理部４５０とを備える。
プロパティ記述入力部４７０は、プロパティ記述４０２を入力する処理を行う。
【００３６】
プロパティ言語情報データベース４０５は、プロパティ言語ごとに、その言語に関する構文ルール、予約語、関数等の情報が格納されているデータベースである。
【００３７】
プロパティ解析処理部４１０は、プロパティ記述４０２を解析する処理を行う。ここでは、プロパティ言語で記載されたプロパティ記述４０２を文字列として解析する。解析処理は、プロパティ言語情報データベース４０５に従って行われる。
【００３８】
仕様書逆生成処理部４２０は、プロパティ解析処理部４１０で解析された結果に基づいて仕様書（自動生成された仕様書４０３に相当）を自動生成すると共に、比較情報データベース４２５を生成する処理を行う。
【００３９】
比較情報データベース４２５は、自動生成された仕様書４０３の情報がそのまま格納されているデータベースである。
仕様書入力部４７１は、設計者が作成した元の仕様書４００を入力する処理を行う。
【００４０】
仕様書比較処理部４３０は、比較情報データベース４２５と設計者が作成した仕様書（元の仕様書４００に相当）とを比較して、相違する箇所及び／または一致する箇所を検出する処理を行う。
なお、相違する箇所のみを検出するようにしてもよいし、一致する箇所のみを検出するようにしてもよいし、何れも検出するようにしてもよい。
【００４１】
修正情報データベース４４０は、仕様書比較処理部４３０が検出した、自動生成された仕様書４０３と元の仕様書４００との相違する箇所及びその内容を格納するデータベースである。つまり、修正情報データベース４４０に格納されている情報は、プロパティ記述の間違い箇所及びその内容ということである。
【００４２】
プロパティ記述修正処理部４５０は、修正情報データベース４４０に格納されている情報からプロパティ記述４０２に記載されている情報を修正し、修正後のプロパティ記述４０４を生成する処理を行う。
【００４３】
ここで、検証支援装置１の処理の流れを説明する。元の仕様書４００は、検証対象となるハードウェアに関する仕様書であり、設計者が作成したものである。検証者は、元の仕様書４００を参照し、プロパティ抽出・翻訳処理部４０１でプロパティの抽出及び翻訳の処理を、マニュアルまたは自動で行い、プロパティ記述４０２を生成する。生成されたプロパティ記述４０２は、プロパティ言語情報データベース４０５が格納する情報に基づいて、プロパティ解析処理部４１０により解析される。解析された情報から仕様書逆生成処理部４２０が自動生成された仕様書４０３を生成する。仕様書比較処理部４３０は、元の仕様書４００と自動生成された仕様書４０３とを比較して相違する箇所を検出し、その相違する箇所と内容を修正情報データベース４４０に格納する。修正情報データベース４４０とプロパティ記述４０２から、プロパティ記述修正処理部４５０が修正後のプロパティ記述４０４を生成する。検証装置４９０には、修正後のプロパティ記述４０４と回路情報４０６が入力され、検証が実行される。
【００４４】
なお、仕様書入力部４７１、仕様書比較処理部４３０、比較情報データベース４２５、修正情報データベース４４０、及び、プロパティ記述修正処理部４５０は必須の構成要素ではなく、実施形態に応じて必要な処理部のみを構成要素としてもよい。例えば、プロパティ記述の入力から仕様書の比較処理までを行い、プロパティの修正処理を行わないような実施形態の場合は、修正情報データベース４４０とプロパティ記述修正処理部４５０は、構成要素から省くことができる。
【００４５】
（３．動作）
以下に、本実施形態に係る検証支援装置１の動作を説明する。
（３−１  仕様書の逆生成処理の動作）
図５は、仕様書を逆生成する処理を示すフローチャートである。まず、検証支援装置１にプロパティ記述４０２が入力される（ステップＳ５０１）。プロパティ解析処理部４１０により、プロパティ言語データベース４０５に基づいてプロパティ記述４０２が解析される（ステップＳ５０２）。具体的には、プロパティ記述４０２から、プロパティ名、入力条件（入力信号名、値等）、及び、出力条件（出力信号名、値等）が抽出される。抽出した入力条件及び出力条件から信号と値を分離し、仕様書には不要となるプロパティ言語の予約語等を削除して表を作成する（ステップＳ５０３）。作成された表を仕様書として生成する（ステップＳ５０４）。作成された仕様書は、自動生成された仕様書４０３として外部に出力されると共に、内部データとして比較情報データベース４２５に格納される。
【００４６】
仕様書の逆生成処理について、さらに詳細に説明する。図６は、元の仕様書４００の一例である。この図では入力信号Ａ、Ｂと出力信号Ｘ、Ｙがあり、入力信号の条件（値）に対する出力条件（値）を示している。図７は、プロパティ記述４０２の一例である。検証者は、図６の仕様書に従って図７のプロパティ記述を生成する。図６の項１、２および３は、それぞれ図７の７００、７１０および７２０のプロパティ記述に翻訳されている。ここでは、本実施形態の特徴をわかりやすく説明するために、図６において、項３の出力信号Ｙの値「２」を、翻訳過程において間違って「３」と記入したと仮定しており、図７のプロパティ記述７２０のＹ＝３は間違って記述しているものとする。
なお、ここでは、プロパティ言語の１つであるＰＳＬで記述しているが、その他のプロパティ言語やライブラリで記述してもよい。
【００４７】
仕様書逆生成手段４２０は、図７に示すプロパティ記述を入力し、各プロパティ記述がプロパティ解析処理部４１０により解析されて、プロパティ名７０１、入力信号と入力条件７０２、及び、出力信号と出力条件７０３がそれぞれ抽出される。すべてのプロパティ記述に対して抽出が完了すると図８に示す仕様書を生成する。図８の８００、８１０、及び、８２０は図７の７００、７１０、及び、７２０に対応する。
【００４８】
このように、プロパティ言語に精通していない人であっても、プロパティ記述の読み難さから開放されるとともに、プロパティ言語を知らない人でもプロパティ記述に存在する翻訳ミスを指摘しやすくなる。また、従来では設計者が作成した元の仕様書４００とプロパティ記述４０２を直接的に比較して等価性を判断することはできなかったが、仕様書を逆生成することで、元の仕様書４００との比較が容易になる。
【００４９】
（３−２  仕様書の比較処理の動作）
図９は、仕様書を比較する処理を示すフローチャートである。まず、元の仕様書４００を仕様書データとして内部データに格納する（ステップＳ９０１）。次に、格納された仕様書データを読み込み（ステップＳ９０２）、比較情報データベース４２５を読み込む（ステップＳ９０３）。ステップＳ９０２で読み込まれた仕様書データの入力条件、及び、出力条件とステップＳ９０３で読み込まれた比較情報データベース４２５に格納された比較情報の入力条件、及び、出力条件について１つずつプロパティ記述を比較し（ステップＳ９０４）、一致していれば、比較情報のプロパティ名を修正情報データベース４４０のプロパティ名の列に格納し、且つ、ステータスを「一致」として格納する（ステップＳ９０５）。不一致であれば、比較情報のプロパティ名を修正情報データベース４４０のプロパティ名の列に格納する。また、比較情報の入力条件、及び、出力条件については、不一致となる箇所のみに、正しい値である仕様書データの値を、修正情報データベース４４０の該当する箇所へ格納する。この時、修正情報データベース４４０のステータスには「修正」として格納する（ステップＳ９０７）。全てのプロパティ記述について比較したかどうかを判定し（ステップＳ９０６）、全て比較していなければステップＳ９０４に戻る。全てを比較していれば比較処理を終了する。
【００５０】
仕様書の比較処理について、さらに詳細に説明する。仕様書比較処理部４３０は、図６に示した仕様書の入力条件、及び、出力条件、並びに、図８に示した逆生成された仕様書の入力条件、及び、出力条件を比較する。ただし、図６の項の番号と図８のプロパティ名は比較対象外とする。このとき図６における項３の出力信号Ｙの値「２」と、図８におけるａｓｓｅｒｔ＿３の出力信号Ｙの値「３」が不一致となる。これは、間接的に図７に示した７２０のプロパティ記述が間違っていることを意味する。そこで仕様書比較処理部４３０は、正しい値である図６における項３の出力信号Ｙの値「２」を修正情報として修正情報データベース４４０に格納する。
【００５１】
図１０は、修正情報データベース４４０に格納された修正情報を表にした具体的な例であり、元の仕様書４００（図６の仕様書）及び自動生成された仕様書４０３（図８の仕様書）を比較した結果と、どのプロパティ記述をどのように修正すればよいかという情報を記憶している。図１０のプロパティ名の列は、図８の仕様書のプロパティ名を記憶している。図１０の入力条件、及び、出力条件の列は、比較結果が一致した場合は空白とし、不一致の場合は、元の仕様書４００に記載されている正しい値を格納する。図１０のステータスの列は比較した結果を表し、任意のプロパティに対して入力条件、及び、出力条件が一致していれば「一致」となり、不一致が１箇所でもあれば「修正」として格納される。ここでは、ａｓｓｅｒｔ＿３の出力信号Ｙの値が、不一致を示す箇所であり、元の仕様書４００から、正しい値「２」を格納している。また、不一致が発生しているのでステータスは「修正」となる。
【００５２】
このように、元の仕様書４００と自動で生成された仕様書４０３とを比較することで、間接的に元の仕様書４００とプロパティ記述４０２の等価性を証明できる。不一致が発生した場合、検証者に対して修正情報を提供し、プロパティ記述４０２の間違っている箇所を通知する。このため検証者は、容易にプロパティ記述４０２の翻訳ミスを発見して修正することができる。
【００５３】
（３−３  プロパティ記述の記載が順不同の場合における仕様書の比較処理の動作）
上記の仕様書の比較処理は、元の仕様書４００とプロパティ記述４０２の順序が同じ場合のみ有効である。すなわち元の仕様書データ４００と比較情報データベース４２５の各プロパティの格納順序が同じでなければならない。しかし、比較情報データベース４２５の元となるプロパティ記述４０２は、検証者が記述するため必ずしも元の仕様書４００の記述順序とプロパティ記述の記述順序が一致するとは限らない。
【００５４】
図１１は、元の仕様書４００と自動生成された仕様書４０３の記述順序が異なる場合の例を示した図である。図１１（ａ）は元の仕様書４００であり、図１１（ｂ）は自動生成された仕様書４０３である。図１１（ａ）の項１に示されたプロパティは図１１（ｂ）に示されたプロパティａｓｓｅｒｔ＿１に対応しており、同様に項２はａｓｓｅｒｔ＿２、項３はａｓｓｅｒｔ＿３にそれぞれ対応しているものとする。また、図１１（ｂ）のａｓｓｅｒｔ＿４に対応するプロパティは図１１（ａ）には存在していない。また、ａｓｓｅｒｔ＿２のプロパティの出力信号Ｘの値は翻訳ミスによって起きた間違いと仮定する。本来なら出力信号Ｘの値は３ではなく、１でなければならない。図１１（ａ）では項１、項２、項３の順で記述されているのに対し、図１１（ｂ）ではａｓｓｅｒｔ＿３、ａｓｓｅｒｔ＿１、ａｓｓｅｒｔ＿２の順で記述されており、プロパティと記述順序が異なっている。このような場合であっても、以下に示す比較処理を行うことで、上記同様の比較を行うことができる。
【００５５】
図１２は、比較する仕様書の記載順序が異なる場合の比較処理を示すフローチャートである。まず、比較情報データベース４２５からプロパティを１つ読み込み、同時にカウンタ変数ｎを０に設定する（ステップＳ１２０１）。次に、カウンタ変数ｎに１を加え、元の仕様書４００の仕様書データからｎ番目のプロパティを１つ読み込む（ステップＳ１２０２）。読み込んだそれぞれのプロパティの入力条件（値）を比較し（ステップＳ１２０３）、入力条件が一致していなければ、仕様書データのすべてのプロパティ読んだかどうかを判定し（ステップＳ１２０４）、すべてのプロパティを読んでいなければステップＳ１２０２へ戻って仕様書データの次のプロパティを読み込む。すべてのプロパティを読んでいれば、ステップＳ１２０１で読み込んだ比較情報データベース４２５のプロパティが仕様書データのどのプロパティにも一致しないことを示す。すなわち、検証者が間違ってプロパティ記述４０２に記述したものであり、作成したプロパティ記述４０２から削除しなければならない。したがって、ステップＳ１２０１で読み込んだ比較情報データベース４２５のプロパティ名を修正情報データベース４４０に格納すると共に、ステータスを「削除」にして（ステップＳ１２０５）、ステップＳ１２０１の処理に戻る。
【００５６】
ステップＳ１２０３で入力条件が一致していれば、同プロパティの出力条件（値）を比較する（ステップＳ１２０６）。出力条件が一致していれば、元の仕様書４００と検証者が記述したプロパティ記述４０２は論理的に等しいため、正しいプロパティと判断できる。そこで、ステップＳ１２０１で読み込んだプロパティのプロパティ名を、修正情報データベース４４０に格納し、同時にステータスを「一致」とする（ステップＳ１２０７）。出力条件が一致していなければ、検証者が作成したプロパティ記述４０２の出力条件が間違っていると判断できるため、ステップＳ１２０１で読み込んだプロパティのプロパティ名とステップＳ１２０２で読み込んだプロパティの正しい出力条件（値）を修正情報データベース４４０へ記憶すると共に、ステータスを「修正」とする（ステップＳ１２０８）。最後に、比較情報データベース４２５のプロパティを、すべて読み終えたかどうかを判定し（ステップＳ１２０９）、すべて読んでいなければステップＳ１２０１の処理に戻る。すべて読んでいれば比較処理を終了する。
【００５７】
ここでは、元の仕様書４００のプロパティと自動生成された仕様書４０３のプロパティの対応付けを入力条件で行っている。もし、自動生成された仕様書４０３のプロパティの入力条件が元の仕様書４００のどのプロパティの入力条件にも一致しない場合は、修正情報データベース４４０のステータスを「削除」とし、後述するプロパティ記述修正処理において、プロパティ記述４０２から該当プロパティを削除するよう促す。
【００５８】
図１３は、上記比較処理を実行した結果、生成された修正情報データベース４４０の情報の例である。図１３において、ａｓｓｅｒｔ＿３、及び、ａｓｓｅｒｔ＿１のプロパティは比較した結果が一致するためステータスが「一致」となっている。ａｓｓｅｒｔ＿２のプロパティは出力信号Ｘが不一致となったため、ステータスが「修正」となる。また、ａｓｓｅｒｔ＿４のプロパティについて、これに対応するプロパティが図１１（ａ）の仕様書に存在しないためステータスが「削除」となる。
このように、本実施形態では、元の仕様書４００のプロパティと自動生成された仕様書４０３のプロパティの記述順序が異なっている場合でも仕様書の比較が可能となる。
【００５９】
（３−４  プロパティ記述修正処理の動作）
図１４は、プロパティ記述を修正する処理を示すフローチャートである。まず、修正情報データベース４４０を読み込む（ステップＳ１４０１）。次に、プロパティ記述４０２を読み込む（ステップＳ１４０２）。修正情報のステータスが「一致」でないかどうかを判定し（ステップＳ１４０３）、「一致」でない場合は、該当するプロパティ記述を修正または削除して（ステップＳ１４０４）、次のステップＳ１４０５に進む。修正情報のステータスが「修正」場合、修正情報のプロパティ名を用いてステップＳ１４０２で読み込んだプロパティ記述４０２を検索し、該当するプロパティ記述の値を修正情報に格納されている正しい値に修正する。また、修正情報のステータスが「削除」だった場合は同様に該当するプロパティ記述を検索し、削除する。ステップＳ１４０３で、修正情報のステータスが「一致」の場合は、何もせずに次のステップＳ１４０５に進む。ステップＳ１４０５では、修正情報のすべてについて処理が行われたかどうかが判定され（ステップＳ１４０６）、すべての修正情報について処理が行われていない場合は、ステップＳ１４０３の処理に戻って、次の修正情報について処理を行う。すべての修正情報について処理が行われている場合は、修正後のプロパティ記述４０４を出力して、プロパティ記述修正処理を終了する。
【００６０】
プロパティ記述の修正処理について、さらに詳細に説明する。プロパティ記述修正処理部４５０は、図７に示したプロパティ記述４０２と図１０に示した修正情報を読み込む。図１０の修正情報において、ステータスが「一致」となっているプロパティ（ａｓｓｅｒｔ＿１、ａｓｓｅｒｔ＿２）については、何も処理を行わない。一方、ステータスが「修正」となっているプロパティ（ａｓｓｅｒｔ＿３）については、出力信号Ｙの値に「２」が格納されているため、図７に示すプロパティ記述４０２のａｓｓｅｒｔ＿３に対して、Ｙ＝２という修正を行う。図１５は、修正後のプロパティ記述４０４である。１５００、及び、１５１０のプロパティ記述は何も修正されていない。一方、１５２０のプロパティ記述はＹ＝２に修正されている。そして、プロパティ記述修正処理部４５０は、修正後のプロパティ記述４０４を出力する。
【００６１】
このように、入力されたプロパティ記述４０２の間違った箇所を修正し、元の仕様書４００と論理的に等価な正しい修正後のプロパティ記述４０４を出力することができる。この修正後のプロパティ記述４０４を用いることにより検証者は回路情報４０６を検証装置４９０により、正しく検証することができるようになる。
【００６２】
（その他の実施形態）
（１．構成と機能）
（１−１  検証支援装置のハードウェア構成）
本実施形態に係る検証支援装置のハードウェア構成は、第１の実施形態と同様であるため説明は省略する。
【００６３】
（１−２  検証支援装置のモジュール構成と機能）
図１６は、本実施形態に係る検証支援装置１のモジュール構成図である。第１の実施形態と異なる点は、併合処理部１６１０を新たに備えている点である。
併合処理部１６１０は、仕様書逆生成処理部４２０で生成された比較情報データベース４２５の比較情報のうち、入力条件（値）が全く同じであるテストケースについて、それぞれのプロパティを併合する処理を行う。
【００６４】
なお、併合した結果は比較情報データベース４２５にフィードバックされてもよいし、プロパティ記述４０２にフィードバックされてもよいし、どちらにもフィードバックされてもよい。比較情報データベース４２５にフィードバックされた場合は、そのまま比較処理を行う。プロパティ記述４０２にフィードバックされた場合は、再度仕様書の逆生成処理を行って、新たな比較情報データベース４２５を生成する。
【００６５】
（２．動作）
図１７は、併合処理を示すフローチャートである。まず、比較情報データベース４２５から１つのプロパティ（プロパティＡとする）を読み込む（ステップＳ１７０１）。プロパティＡ以降のプロパティを１つ読み込む（ステップＳ１７０２）。読み込んだそれぞれのプロパティの入力条件の値を比較し（ステップＳ１７０３）、不一致であれば、ステップＳ１７０２に戻って、次のプロパティを読み込む。一致していれば、それぞれの出力条件を併合し、１つのプロパティとする（ステップＳ１７０４）。この時、プロパティ記述４０２における該当するプロパティ記述を併合して修正する。その場合、比較情報のプロパティ名からプロパティ記述４０２の該当するプロパティを検出して修正を行う。
なお、この時、比較情報データベース４２５を併合した結果に基づいて修正するようにしてもよい。
【００６６】
プロパティＡ以降のすべてのプロパティを読んだかを判定し（ステップＳ１７０５）、読んでいなければ、ステップＳ１７０２の処理に戻って、次のプロパティを読み込む。読んでいれば、すべてのプロパティについて処理が行われたかどうかを判定し（ステップＳ１７０６）、すべてのプロパティについて処理が行われていなければ、ステップＳ１７０１の処理に戻って、次のプロパティをプロパティＡとして読み込む。すべてのプロパティについて処理が行われていれば、併合処理を終了する。
【００６７】
併合処理について、さらに詳細に説明する。図１８は、併合処理の詳細を示す図である。図１８（ａ）は、図６に示した元の仕様書４００のプロパティ記述である。このプロパティ記述では、項１のプロパティを２つのプロパティ記述（１８０１、１８０２）で表現している。１８０１は、「入力信号Ａが０かつ入力信号Ｂが０の条件のとき、出力信号Ｘは常に１である」というプロパティであり、出力信号Ｙについて出力条件を定義していない。また、１８０２は、「入力信号Ａが０かつ入力信号Ｂが０の条件のとき、出力信号Ｙは常に０である」というプロパティであり、出力信号Ｘについては出力条件を定義していない。これらを併せて解釈すれば「入力信号Ａが０かつ入力信号Ｂが０の条件のとき、出力信号Ｘが常に１で出力信号Ｙは常に０である」と同意である。つまり、内容的には元の仕様書４００と同じであるが、プロパティ記述４０２の表現が異なっている。このような状況は、特に検証者がプロパティ記述４０２を作成する場合に起こり得る。
【００６８】
図１８（ａ）のプロパティ記述に基づいて逆生成した仕様書が図１８（ｂ）である。図１８（ｂ）では、プロパティ１８０１と１８０２が別々のプロパティとして仕様書に記載される。つまり、この状態で元の仕様書４００と比較処理を行うと、いずれも元の仕様書４００と相違し、修正対象となってしまう。そこで、この生成されたデータ情報（比較情報データベース４２５に格納された比較情報）に基づいて併合処理を行った結果が図１８（ｃ）または図１８（ｄ）である。図１８（ｃ）は、比較情報データベース４２５の比較情報を併合した結果であり、図１８（ｄ）は、プロパティ記述４０２を併合した結果である。図１８（ｄ）のプロパティ記述は、再度仕様書の逆生成処理を行うことで、図１８（ｃ）と同じ結果が得られる。図１８（ｃ）の比較情報と元の仕様書４００を比較すると、プロパティ１８０３のステータスは「一致」となり、上記のような問題の発生を防止することができる。
このように、元の仕様書４００と内容は同じであるが表現が異なるような場合であっても、プロパティ記述を併合することで元の仕様書４００と一致させることができる。
【００６９】
以上の前記各実施形態により本発明を説明したが、本発明の技術的範囲は実施形態に記載の範囲には限定されず、これら各実施形態に多様な変更又は改良を加えることが可能である。そして、かような変更又は改良を加えた実施の形態も本発明の技術的範囲に含まれる。このことは、特許請求の範囲及び課題を解決する手段からも明らかなことである。
【図面の簡単な説明】
【００７０】
【図１】設計者が作成した仕様書と検証対象となるハードウェアの一例を示す図である。
【図２】ＰＳＬを用いたプロパティ記述の一例を示す図である。
【図３】第１の実施形態に係る検証支援装置のハードウェアの構成図である。
【図４】第１の実施形態に係る検証支援装置のモジュール構成図である。
【図５】仕様書を逆生成する処理を示すフローチャートである。
【図６】設計者が作成した元の仕様書の一例を示す図である。
【図７】プロパティ記述の一例を示す図である。
【図８】逆生成された仕様書の一例を示す図である。
【図９】仕様書を比較する処理を示すフローチャートである。
【図１０】修正情報データベースに格納された修正情報の一例を示す図である。
【図１１】記述順序が異なる場合の元の仕様書と自動生成された仕様書との一例を示す図である。
【図１２】比較する仕様書の記載順序が異なる場合の比較処理を示すフローチャートである。
【図１３】修正情報データベースに格納された修正情報の一例を示す図である。
【図１４】プロパティ記述を修正する処理を示すフローチャートである。
【図１５】修正後のプロパティ記述の一例を示す図である。
【図１６】その他の実施形態に係る検証支援装置のモジュール構成図である。
【図１７】併合処理を示すフローチャートである。
【図１８】併合処理の詳細を示す図である。
【符号の説明】
【００７１】
１  検証支援装置
３０１  ＣＰＵ
３０２  ＲＡＭ
３０３  ＲＯＭ
３０４  フラッシュメモリ
３０５  ＨＤ
３０６  ＬＡＮカード
３０７  マウス
３０８  キーボード
３０９  ビデオカード
３０９ａ  ディスプレイ
３１０  サウンドカード
３１０ａ  スピーカ
３１１  ドライブ
４００  元の仕様書
４０１  プロパティ抽出・翻訳処理部
４０２  プロパティ記述
４０３  自動生成された仕様書
４０４  修正後のプロパティ記述
４０５  プロパティ言語情報データベース
４０６  回路情報
４１０  プロパティ解析処理部
４２０  仕様書逆生成処理部
４２５  比較情報データベース
４３０  仕様書比較処理部
４４０  修正情報データベース
４５０  プロパティ記述修正処理部
４７０  プロパティ記述入力部
４７１  仕様書入力部
４９０  検証装置
１６１０  併合処理部
【図１】
2009086918.tif 000003
【図２】
2009086918.tif 000004
【図３】
2009086918.tif 000005
【図４】
2009086918.tif 000006
【図５】
2009086918.tif 000007
【図６】
2009086918.tif 000008
【図７】
2009086918.tif 000009
【図８】
2009086918.tif 000010
【図９】
2009086918.tif 000011
【図１０】
2009086918.tif 000012
【図１１】
2009086918.tif 000013
【図１２】
2009086918.tif 000014
【図１３】
2009086918.tif 000015
【図１４】
2009086918.tif 000016
【図１５】
2009086918.tif 000017
【図１６】
2009086918.tif 000018
【図１７】
2009086918.tif 000019
【図１８】
2009086918.tif 000020