修正プログラム、修正装置、および修正方法
【課題】アサーションの修正作業の効率化を図ること。
【解決手段】アサーションＡ５は、対象回路ＤＵＴの設計情報１０１によるシミュレーションで不成立となったアサーションである。修正装置１００で分解されたプロパティｐ１〜ｐ４は、アサーションＡ５の論理構造にしたがって木構造データＴ５となる。プロパティｐ１〜ｐ４は、テストベンチ１０２に組み込まれ、対象回路ＤＵＴのシミュレーションにより、成立、不成立が判断される。修正装置１００は、プロパティｐ１に、「｜｜Ｘ」を追加することで、プロパティｐ１を修正する。したがって、修正後にシミュレーションすると、クロックの立ち上がり時に、レジスタＲｂ，Ｒｃのビット値Ｂ，Ｃは「０」、レジスタＲｘのビット値Ｘは「１」になった場合、修正プロパティＰ１は成立する。
【解決手段】アサーションＡ５は、対象回路ＤＵＴの設計情報１０１によるシミュレーションで不成立となったアサーションである。修正装置１００で分解されたプロパティｐ１〜ｐ４は、アサーションＡ５の論理構造にしたがって木構造データＴ５となる。プロパティｐ１〜ｐ４は、テストベンチ１０２に組み込まれ、対象回路ＤＵＴのシミュレーションにより、成立、不成立が判断される。修正装置１００は、プロパティｐ１に、「｜｜Ｘ」を追加することで、プロパティｐ１を修正する。したがって、修正後にシミュレーションすると、クロックの立ち上がり時に、レジスタＲｂ，Ｒｃのビット値Ｂ，Ｃは「０」、レジスタＲｘのビット値Ｘは「１」になった場合、修正プロパティＰ１は成立する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、情報を修正する修正プログラム、修正装置、および修正方法に関する。
【背景技術】
【０００２】
従来、シミュレーション結果履歴として、不合格となったアサーション及び合格となったアサーションを特定するための「不合格が発生した回数」、「不合格が発生した時刻に関する情報」などを記憶する技術が開示されている。また、シミュレーションでエラーが発生した場合に、テストプログラムのどのパターンでエラーが発生したかを解析し、解析したエラー発生パターンを表示する技術も開示されている。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２００８−１５８６９６号公報
【特許文献２】特開２００２−１４９４４０号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
アサーションの作成元となる仕様書について、検証者が理解不足であったり誤解している場合、作成されたアサーションに誤りが存在する。このようなアサーションを用いて対象回路のシミュレーションを実行して、アサーションが不成立になった場合、アサーションが正しくて不成立になったかアサーションに誤りがあったために不成立になったかの判別がつかない。また、不成立の原因となるシミュレーション結果は、アサーションの内容により複数とおり出現することもある。
【０００５】
したがって、検証者が自ら仕様書を再分析して、または検証者が設計者とともに仕様書を再確認し、その上でアサーションを修正する必要がある。これにより、アサーションの修正作業に時間がかかる。
【０００６】
また、上述した従来技術では、アサーション自体が正しいものであるとの前提で処理をおこなっているため、仕様書の理解不足や誤解に基づくアサーションの誤りを特定することは困難である。
【０００７】
本発明の一側面では、アサーションの修正作業の効率化を図ることができる修正プログラム、修正装置、および修正方法を提供することを目的とする。
【課題を解決するための手段】
【０００８】
本発明の一側面として、修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解し、対象回路のシミュレーションを実行することにより、前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出し、検出された不成立になったプロパティに、不成立の原因要素を論理和で結合し、結合されたプロパティを出力する修正プログラム、修正装置、および修正方法が提案される。
【発明の効果】
【０００９】
本発明の一側面によれば、アサーションの修正作業の効率化を図ることができるという効果を奏する。
【図面の簡単な説明】
【００１０】
【図１】図１は、本実施の形態にかかるアサーション修正例を示す説明図である。
【図２】図２は、修正対象の絞込み例を示す説明図である。
【図３】図３は、シミュレーション結果２００の選択画面例を示す説明図である。
【図４】図４は、木構造データを示す説明図である。
【図５】図５は、修正対象アサーションから分解されたプロパティ群での対象回路ＤＵＴの再シミュレーション結果５００を示す説明図である。
【図６】図６は、プロパティ修正例を示す説明図（その１）である。
【図７】図７は、プロパティ修正例を示す説明図（その２）である。
【図８】図８は、プロパティ修正例を示す説明図（その３）である。
【図９】図９は、実施の形態にかかる修正装置１００のハードウェア構成例を示すブロック図である。
【図１０】図１０は、修正装置１００の機能的構成を示すブロック図である。
【図１１】図１１は、修正装置１００による修正処理手順を示すフローチャートである。
【図１２】図１２は、図１１に示した修正処理（ステップＳ１１０９）の詳細な処理手順例を示すフローチャートである。
【発明を実施するための形態】
【００１１】
以下に添付図面を参照して、この発明にかかる修正プログラム、修正装置、および修正方法の実施の形態を詳細に説明する。
【００１２】
本実施の形態では、対象回路のシミュレーションにより不成立（失敗）となったアサーションを修正対象とする。ここで、アサーションとは、対象回路の設計が満たすべき性質を記述した情報である。ＳＶＡ（Ｓｙｓｔｅｍ Ｖｅｒｉｌｏｇ Ａｓｓｅｒｔｉｏｎ）を例に挙げると、プロパティとして「Ａ＝＝Ｂ」が記述されている場合、変数／信号Ａが常に変数／信号Ｂと同じであることを確認すべきことを意味している。
【００１３】
また、プロパティとして「Ａ｜−＞Ｂ」が記述されている場合、イベントＡが発生した場合、イベントＢが発生することを確認すべきことを意味している。また、プロパティとして「Ａ＆＆Ｂ」が記述されている場合、ビット値Ａおよびビット値Ｂが常に「１」に設定されることを確認すべきことを意味している。
【００１４】
アサーションが成立していれば、対象回路は仕様書どおりに振舞っていることがわかる。一方、アサーションが不成立であれば、対象回路は仕様書どおりに動作していないことがわかる。ここで、検証者が対象回路の仕様書について理解不足であったり、誤解をしていた場合、アサーションが不成立になっても、仕様書にはない動作による不成立であるか仕様書どおりの動作であるにもかかわらずアサーションの誤りによる不成立であるかの判別がつかない。そこで、本実施の形態では、不成立のあったアサーションについて、不成立の原因となった要素（変数、信号、ビット値）を不成立のあったアサーションに対し論理和で追加する。
【００１５】
また、アサーション自体は、複雑な記述や冗長な記述となっている場合が多い。したがって、不成立となったアサーションのどの箇所を修正すべきか検証者が確認する必要がある。したがって、本実施の形態では、シミュレーションに先立って、アサーションを分解する。本実施の形態では、分解された記述を「プロパティ」と称す。プロパティは、上述した「Ａ＝＝Ｂ」、「Ａ｜−＞Ｂ」、「Ａ＆＆Ｂ」のような単純な式である。したがって、シミュレーションにおいて不成立となったプロパティに対し修正したり修正案を提示することで、修正作業の効率化を図る。
【００１６】
＜アサーション修正例＞
図１は、本実施の形態にかかるアサーション修正例を示す説明図である。図１において、アサーションＡ５は、対象回路ＤＵＴの設計情報１０１によるシミュレーションで不成立となったアサーションである。アサーションＡ５は、複数のプロパティｐ１〜ｐ４が論理和（｜｜）または論理積（＆＆）で結合された情報である。
【００１７】
したがって、修正装置１００は、アサーションＡ５を論理和および論理積の箇所を境界にして分解する。図１では、アサーションＡ５は、プロパティｐ１〜ｐ４に分解される。分解されたプロパティｐ１〜ｐ４は、アサーションＡ５の論理構造にしたがって木構造データＴ５となる。
【００１８】
プロパティｐ１〜ｐ４は、テストベンチ１０２に組み込まれ（図１では例としてｐ１）、対象回路ＤＵＴの設計情報１０１を用いた対象回路ＤＵＴのシミュレーションにより、成立、不成立が判断される。たとえば、クロックの立ち上がり時に、レジスタＲｂ，Ｒｃのビット値Ｂ，Ｃが「０」、レジスタＲｘのビット値Ｘが「１」になった場合、プロパティｐ１は不成立となる。
【００１９】
この場合、修正装置１００は、プロパティｐ１に、「｜｜Ｘ」を追加することで、プロパティｐ１を修正する。したがって、修正後にシミュレーションを実行すると、クロックの立ち上がり時に、レジスタＲｂ，Ｒｃのビット値Ｂ，Ｃが「０」、レジスタＲｘのビット値Ｘが「１」になった場合、修正プロパティＰ１は成立することになる。
【００２０】
＜修正対象の絞込み例＞
図２は、修正対象の絞込み例を示す説明図である。図２では、図１のアサーションの分解に先立って、修正対象のアサーションを絞り込む。これにより、誤りが潜んでいる可能性が高いアサーションを優先的に抽出することができる。
【００２１】
具体的には、アサーション群が組み込まれたテストベンチ１０２と対象回路ＤＵＴの設計情報１０１とを用いた対象回路ＤＵＴのシミュレーションにより、修正装置１００は、シミュレーション結果２００を得る。シミュレーション結果２００では、アサーションごとにアサーションＩＤと不成立回数が記憶されている。アサーションＩＤは、アサーションを特定する識別コードである。本例では、説明の都合上、アサーションに割り当てた符号を識別コードとしている。
【００２２】
不成立回数とは、シミュレーション時にアサーションが成立しなかった回数であり、シミュレーション中に計数される。この不成立回数には、不成立の原因が複数とおりある場合、それらの不成立回数が混在する。たとえば、アサーションＡ５の不成立回数は２０であるが、プロパティｐ１〜ｐ４での不成立回数の合計が２０回であることを意味しており、内訳はプロパティごとに異なる。
【００２３】
たとえば、プロパティｐ１が１３回、プロパティｐ２が７回、プロパティｐ３，ｐ４が０回である場合、プロパティｐ３，ｐ４については修正する必要がないことがわかる。このように、アサーションを分解することで、修正すべきプロパティと修正すべきでないプロパティを特定することができる。
【００２４】
図３は、シミュレーション結果２００の選択画面例を示す説明図である。図３では、シミュレーション結果２００が選択画面３００に表示されている。具体的には、たとえば、アサーションごとに、アサーションＩＤと不成立回数とチェックボックスとが表示されている。不成立回数が多いアサーションほど誤りが潜んでいる可能性が高い。したがって、検証者は、マウスなどの入力装置を操作して、修正したいアサーションのチェックボックス３０１にチェックを入れて、確認ボタン３０２を押下することで、修正対象アサーションが決定される。
【００２５】
図３の場合、アサーションＡ５，Ａ７，Ａ４，Ａ２が修正対象アサーションとなる。なお、図２および図３では、不成立回数を記憶、表示させているが、不成立確率（＝不成立回数／（成立回数＋不成立回数））を記憶、表示させることとしてもよい。
【００２６】
図４は、木構造データを示す説明図である。木構造データは、図１に示したように、アサーションをその論理構造で分解し、関連しあうプロパティを連結した構造体である。図４において、○は木構造データの節点であり、プロパティを示す。○内の符号でプロパティを示している。木構造データは修正対象アサーションごとに生成される。各木構造データの最上位階層を第１階層とし、階層が下がるごとに階層番号ｒが増加する。図４の場合は、アサーションＡ７の第５階層が最下位階層となる。
【００２７】
図５は、修正対象アサーションから分解されたプロパティ群での対象回路ＤＵＴの再シミュレーション結果５００を示す説明図である。図５では、プロパティごとに、プロパティＩＤ、不成立回数、および不成立原因要素が記憶される。プロパティＩＤは、プロパティを特定する識別コードである。本例では、説明の都合上、プロパティに割り当てた符号を識別コードとしている。不成立回数とは、シミュレーション時にプロパティが成立しなかった回数であり、再シミュレーション中に計数される。
【００２８】
不成立原因要素とは、プロパティが不成立となった原因を示す要素である。たとえば、プロパティｐ１の不成立原因要素は「Ｘ」となっている。すなわち、レジスタＲｂ，Ｒｃのビット値ＢまたはＣの少なくともいずれか一方が「１」になるべきところ、いずれも「０」で、レジスタＲＸのビット値Ｘが「Ｘ＝１」になったために、不成立になったことを示している。
【００２９】
また、プロパティｐ２の不成立原因要素は「Ｅ＝＝３」となっている。すなわち、プロパティｐ２ではＤ＝１の１サイクル後にＥ＝＝２となるべきところ、「Ｅ＝＝３」になったために、不成立になったことを示している。
【００３０】
また、プロパティｐ５の不成立原因要素は「Ｇ＝＝Ｊ」となっている。すなわち、プロパティｐ５では、変数／信号Ｇが常に変数／信号Ｈと同じであるべきところ、「Ｇ＝＝Ｊ」になったために、不成立になったことを示している。
【００３１】
＜プロパティ修正例＞
図６〜図８は、プロパティ修正例を示す説明図である。図６は、プロパティｐ２の修正例を示している。プロパティｐ２では、Ｄ＝１の１サイクル後にＥ＝＝２となるべきところ、「Ｅ＝＝３」になったために、不成立になっている。したがって、修正装置１００は、プロパティｐ２に不成立原因要素である「Ｅ＝＝３」を論理和で結合する。これにより、プロパティｐ２が修正プロパティＰ２となる。したがって、次回のシミュレーションで、Ｄ＝＝１の１サイクル後は、「Ｅ＝＝２」または「Ｅ＝＝３」のいずれかになれば、修正プロパティＰ２が成立することになる。
【００３２】
図７は、プロパティｐ１の修正例を示している。プロパティｐ１では、レジスタＲｂ，Ｒｃのビット値ＢまたはＣの少なくともいずれか一方が「１」になるべきところ、いずれも「０」で、レジスタＲＸのビット値ｘが「Ｘ＝１」になったために、不成立になっている。したがって、修正装置１００は、プロパティｐ１に不成立原因要素である「Ｘ」を論理和で結合する。これにより、プロパティｐ１が修正プロパティＰ１となる。したがって、次回のシミュレーションで、レジスタＲｂ，Ｒｃ，Ｒｘのビット値Ｂ，ＣまたはＸの少なくともいずれか一つが「１」になれば、修正プロパティＰ１が成立することになる。
【００３３】
図８は、プロパティｐ５の修正例を示している。プロパティｐ５では、変数／信号Ｇが常に変数／信号Ｈと同じであるべきところ、「Ｇ＝＝Ｊ」になったために、不成立になっている。したがって、修正装置１００は、プロパティｐ５に不成立原因要素である「Ｇ＝＝Ｊ」を論理和で結合する。これにより、プロパティｐ５が修正プロパティＰ５となる。したがって、次回のシミュレーションで、「Ｇ＝＝Ｈ」または「Ｇ＝＝Ｊ」のいずれかになれば、修正プロパティＰ５が成立することになる。
【００３４】
＜修正装置１００のハードウェア構成例＞
図９は、実施の形態にかかる修正装置１００のハードウェア構成例を示すブロック図である。図９において、修正装置１００は、ＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）９０１と、ＲＯＭ（Ｒｅａｄ‐Ｏｎｌｙ Ｍｅｍｏｒｙ）９０２と、ＲＡＭ（Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）９０３と、磁気ディスクドライブ９０４と、磁気ディスク９０５と、光ディスクドライブ９０６と、光ディスク９０７と、ディスプレイ９０８と、Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）９０９と、キーボード９１０と、マウス９１１と、スキャナ９１２と、プリンタ９１３と、を備えている。また、各構成部はバス９００によってそれぞれ接続されている。
【００３５】
ここで、ＣＰＵ９０１は、修正装置１００の全体の制御を司る。ＲＯＭ９０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ９０３は、ＣＰＵ９０１のワークエリアとして使用される。磁気ディスクドライブ９０４は、ＣＰＵ９０１の制御にしたがって磁気ディスク９０５に対するデータのリード／ライトを制御する。磁気ディスク９０５は、磁気ディスクドライブ９０４の制御で書き込まれたデータを記憶する。
【００３６】
光ディスクドライブ９０６は、ＣＰＵ９０１の制御にしたがって光ディスク９０７に対するデータのリード／ライトを制御する。光ディスク９０７は、光ディスクドライブ９０６の制御で書き込まれたデータを記憶したり、光ディスク９０７に記憶されたデータをコンピュータに読み取らせたりする。
【００３７】
ディスプレイ９０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ９０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００３８】
インターフェース（以下、「Ｉ／Ｆ」と略する。）９０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ Ａｒｅａ Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ Ａｒｅａ Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク９１４に接続され、このネットワーク９１４を介して他の装置に接続される。そして、Ｉ／Ｆ９０９は、ネットワーク９１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ９０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００３９】
キーボード９１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス９１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００４０】
スキャナ９１２は、画像を光学的に読み取り、修正装置１００内に画像データを取り込む。なお、スキャナ９１２は、ＯＣＲ（Ｏｐｔｉｃａｌ Ｃｈａｒａｃｔｅｒ Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ９１３は、画像データや文書データを印刷する。プリンタ９１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００４１】
＜修正装置１００の機能的構成例＞
図１０は、修正装置１００の機能的構成を示すブロック図である。修正装置１００は、実行部１００１と、取得部１００２と、選択部１００３と、分解部１００４と、生成部１００５と、検出部１００６と、結合部１００７と、算出部１００８と、判断部１００９と、出力部１０１０と、を備えている。実行部１００１〜出力部１０１０は、は、具体的には、たとえば、図９に示したＲＯＭ９０２、ＲＡＭ９０３、磁気ディスク９０５、光ディスク９０７などの記憶装置に記憶されたプログラムをＣＰＵ９０１に実行させることにより、または、Ｉ／Ｆ９０９により、その機能を実現する。
【００４２】
実行部１００１は、対象回路ＤＵＴの設計情報１０１によるシミュレーションを実行する。具体的には、たとえば、図２に示したように、実行部１００１は、シミュレーションを実行する。また、実行部１００１は、シミュレーション中に、アサーションが成立（成功）するか不成立になる（失敗）かを判断する。不成立の場合は、アサーションごとに不成立回数を計数して、図２に示したようにシミュレーション結果２００として記憶装置に記憶する。
【００４３】
取得部１００２は、対象回路ＤＵＴのシミュレーションを実行することによりアサーションごとの不成立回数を取得する。具体的には、たとえば、図２に示したシミュレーション結果２００が実行部１００１により記憶装置に記憶されるため、取得部１００２は、記憶装置のシミュレーション結果２００の中からアサーションごとの不成立回数を読み出す。
【００４４】
選択部１００３は、取得部１００２によって取得された不成立回数に基づいてアサーション群の中から修正対象アサーションを選択する。具体的には、たとえば、取得部１００２によって取得された不成立回数に基づいて図３に示した選択画面３００が表示される。したがって、検証者は、マウス９１１などの入力装置を操作して修正したいアサーションのチェックボックス３０１にチェックを入れ、確認ボタン３０２を押下する。これにより、選択部１００３は、チェックボックス３０１にチェックが入れられたアサーションを修正対象アサーションであると認識する。
【００４５】
分解部１００４は、修正対象アサーションをアサーションの論理構造に基づいて分解する。分解対象となる修正対象アサーションは、検証者が任意に決めてもよく、また、選択部１００３によって選択されたアサーションを修正対象アサーションとしてもよい。分解部１００４では、図１に示したように、論理和または論理積で結合されている式をプロパティとして抽出する。抽出されたプロパティ群は修正対象アサーションごとに記憶装置に記憶される。
【００４６】
生成部１００５は、分解部１００４によって分解されたプロパティ群の木構造データを生成する。具体的には、たとえば、生成部１００５は、修正対象アサーションごとに得られたプロパティ群内の包含関係により木構造データを生成する。たとえば、プロパティｐ４にはプロパティｐ２，ｐ３が包含されているため、プロパティｐ２，ｐ３は、プロパティｐ４の下位階層のプロパティとして連結される。プロパティｐ３にはプロパティｐ１が包含されているため、プロパティｐ１は、プロパティｐ３の下位階層のプロパティとして連結される。これにより、図４に示したような木構造データが修正対象プロパティごとに生成されることになる。
【００４７】
また、実行部１００１は、図１に示したように、分解されたプロパティ群を用いて対象回路ＤＵＴのシミュレーション（再シミュレーション）を実行する。再シミュレーションでは、プロパティごとに不成立回数を計数し、不成立原因要素を検出する。これにより、図５に示したような再シミュレーション結果５００が得られる。再シミュレーション結果５００は、記憶装置に記憶される。
【００４８】
検出部１００６は、対象回路ＤＵＴのシミュレーションを実行することにより、分解部１００４によって修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出する。具体的には、たとえば、検出部１００６は、再シミュレーション結果５００の中で所定回数（たとえば１回）以上不成立となったプロパティを修正対象プロパティとして検出する。
【００４９】
また、検出部１００６は、生成部１００５によって生成された木構造データを構成するプロパティ群のうち最下層のプロパティから検出する。たとえば、図４の例では、第５階層のプロパティｐ５，ｐ６を検出し、つぎに、第４階層のプロパティｐ７，ｐ１１を検出し、つぎに、第３階層のプロパティｐ１、ｐ８、ｐ１２〜ｐ１４を検出する。このように、段階的に階層を上げていき、検出部１００６は、最終的に第１階層のプロパティｐ４、ｐ１０、ｐ１７，１８を検出することになる。また、検出部１００６は、再シミュレーション結果５００から修正対象プロパティの不成立原因要素を検出する。
【００５０】
結合部１００７は、検出部１００６によって検出された不成立になったプロパティに、不成立の原因要素を論理和で結合する。結合部１００７は、具体的には、たとえば、図６〜図８に示したように、論理和で結合する。
【００５１】
算出部１００８は、修正対象アサーションごとに、結合部１００７によって結合する都度、結合されたプロパティについての結合前の不成立回数を累積する。たとえば、修正対象アサーションＡ５のプロパティｐ１〜ｐ４を例に挙げると、修正対象アサーションＡ５の不成立回数は２０回（図２を参照）であり、プロパティｐ１の不成立回数は１３回、プロパティｐ２の不成立回数は７回、プロパティｐ３，ｐ４の不成立回数はともに０回である（図５を参照）。
【００５２】
まず、累積不成立回数の初期値は０である。検出部１００６は、最下層である第５階層から順次修正対象プロパティを検出するため、修正対象アサーションＡ５の木構造データＴ５については、第３階層のプロパティｐ１が最初に検出されて、結合部１００７により結合が行われる。このとき、プロパティｐ１の不成立回数は１３回であるため、累積不成立回数に累積することで、０＋１３＝１３回となる。つぎに、第２階層のプロパティｐ２が検出されて、結合部１００７により結合が行われる。このとき、プロパティｐ２の不成立回数は７回であるため、累積不成立回数に累積することで、１３＋７＝２０回となる。
【００５３】
判断部１００９は、修正対象アサーションごとに、算出部１００８によって累積された不成立回数が、修正対象アサーションの不成立回数に到達したか否かを判断する。具体的には、累積される都度、判断部１００９は、修正対象アサーションの不成立回数に到達したか否かを判断する。
【００５４】
たとえば、上記の例で、第２階層のプロパティｐ２が検出されて、累積不成立回数が、１３＋７＝２０回となった場合、修正対象アサーションＡ５の不成立回数２０回に到達したと判断する。この場合、検出部１００６は、木構造データＴ５については、これ以上、不成立のプロパティｐ３，ｐ４の検出はおこなわない。
【００５５】
すなわち、検出処理を実行しても、不成立のプロパティは得られないため、木構造データＴ５を検出対象から除外する。たとえば、検出不可フラグを設定したり、木構造データＴ５を消去したりする。これにより、修正処理の高速化を図ることができる。
【００５６】
出力部１０１０は、結合部１００７によって結合されたプロパティを出力する。具体的には、たとえば、出力部１０１０は、結合されたプロパティ、すなわち、修正済みのプロパティを出力する。また、修正する必要がなかったプロパティも出力する。これらのプロパティをまとめて修正プロパティ群と称す。修正プロパティ群は、ディスプレイ９０８に出力することで、表示される。また、プリンタ９１３に出力されることで印刷される。また、Ｉ／Ｆ９０９に出力されることで、外部装置に送信される。また、記憶装置に出力されることで、修正プロパティ群が保存される。
【００５７】
＜修正処理手順＞
図１１は、修正装置１００による修正処理手順を示すフローチャートである。まず、修正装置１００は、図２に示したようなシミュレーション結果２００を取得して（ステップＳ１１０１）、不成立回数の降順にアサーションを並び替える（ステップＳ１１０２）。そして、修正装置１００は、図３に示したような、並び替え後のアサーションを示す選択画面３００をディスプレイ９０８に表示する（ステップＳ１１０３）。
【００５８】
修正装置１００は、選択部１００３により選択入力があった場合（ステップＳ１１０４：Ｙｅｓ）、選択アサーションＩＤを保持して（ステップＳ１１０５）、ステップＳ１１０６に移行する。一方、選択入力がない場合（ステップＳ１１０４：Ｎｏ）、ステップＳ１１０６に移行する。
【００５９】
ステップＳ１１０６において、修正装置１００は、選択画面３００の確認ボタン３０２の選択入力による確定選択があったか否かを判断する（ステップＳ１１０６）。確定選択がない場合（ステップＳ１１０６：Ｎｏ）、ステップＳ１１０４に戻る。一方、確定選択があった場合（ステップＳ１１０６：Ｙｅｓ）、修正装置１００は、選択アサーションＩＤがあるか否かを判断する（ステップＳ１１０７）。
【００６０】
選択アサーションＩＤがない場合（ステップＳ１１０７：Ｎｏ）、アサーションを１つも選択せずに確定選択をしたこととなり、一連の処理を終了する。一方、選択アサーションＩＤがある場合（ステップＳ１１０７：Ｙｅｓ）、選択アサーションＩＤを手がかりにして、シミュレーション結果２００から選択アサーションを抽出する（ステップＳ１１０８）。そして、抽出された選択アサーションは修正対象アサーションになるため、修正装置１００は、修正対象アサーションについて修正処理を実行する（ステップＳ１１０９）。修正処理（ステップＳ１１０９）の詳細は図１２で後述する。
【００６１】
修正処理（ステップＳ１１０９）後、修正装置１００は、出力部１０１０により、修正プロパティ群を出力する（ステップＳ１１１０）ことで、一連の処理を終了する。なお、修正プロパティ群については、検証者がマウス９１１やキーボード９１０などの入力装置を操作することで、適宜修正をおこなってもよい。
【００６２】
図１２は、図１１に示した修正処理（ステップＳ１１０９）の詳細な処理手順例を示すフローチャートである。まず、修正装置１００は、未選択の修正対象アサーションがあるか否かを判断する（ステップＳ１２０１）。未選択の修正対象アサーションがある場合（ステップＳ１２０１：Ｙｅｓ）、修正装置１００は、選択部１００３により未選択の修正対象アサーションを選択し（ステップＳ１２０２）、分解部１００４により、修正対象アサーションを分解する（ステップＳ１２０３）。そして、修正装置１００は、生成部１００５により、分解されたプロパティ群で修正対象アサーションの木構造データを生成して（ステップＳ１２０４）、ステップＳ１２０１に戻る。
【００６３】
また、ステップＳ１２０１において、未選択の修正対象アサーションがない場合（ステップＳ１２０１：Ｎｏ）、修正装置１００は、階層番号ｒをｒ＝Ｒに設定する（ステップＳ１２０５）。Ｒは、生成された木構造データ群の最下層である。図４の例ではＲ＝５となる。つぎに、修正装置１００は、実行部１００１により、プロパティ群（木構造データ群）を用いて対象回路ＤＵＴの再シミュレーションを実行する（ステップＳ１２０６）。
【００６４】
そして、修正装置１００は、検出部１００６により、木構造データ群の第ｒ階層のプロパティから不成立のプロパティを検出する（ステップＳ１２０７）。つぎに、修正装置１００は、図６〜図８に示したように、結合部１００７により、不成立のプロパティの不成立原因要素を、論理和で不成立のプロパティに結合する（ステップＳ１２０８）。
【００６５】
そして、修正装置１００は、算出部１００８により修正済みプロパティの不成立回数を修正対象アサーションごとに累積計算する（ステップＳ１２０９）。このあと、修正装置１００は、判断部１００９により、修正対象アサーションごとに、修正対象アサーションの不成立回数に到達したか否かを判断する（ステップＳ１２１０）。到達していない修正対象アサーションについては（ステップＳ１２１０：Ｎｏ）、ステップＳ１２１２に移行する。一方、到達した修正対象アサーションについては（ステップＳ１２１０：Ｙｅｓ）、到達した修正対象アサーションの木構造データを修正対象外に設定し（ステップＳ１２１１）、ステップＳ１２１２に移行する。これにより、以降の修正処理の高速化を図ることができる。
【００６６】
ステップＳ１２１２では、修正装置１００は、階層番号ｒをデクリメントし（ステップＳ１２１２）、ｒ＝０であるか否かを判断する（ステップＳ１２１３）。ｒ＝０でない場合（ステップＳ１２１３：Ｎｏ）、ステップＳ１２０７に戻る。一方、ｒ＝０である場合（ステップＳ１２１３：Ｙｅｓ）、修正処理（ステップＳ１１０９）を終了し、ステップＳ１１１０に移行する。なお、上述した修正処理（ステップＳ１１０９）においては、ステップＳ１２０９〜Ｓ１２１１を省略してもよい。
【００６７】
このように、本実施の形態によれば、不成立となったアサーションをプロパティ群に分解し、不成立のプロパティごとに、不成立原因要素を論理和で結合するため、修正処理の自動化を図ることができる。また、アサーションではなくプロパティ単位で修正処理をおこなうため、修正箇所を人手で探さずに自動で修正箇所を突き止めることができる。したがって、修正処理の高速化を図ることができる。また、木構造データの最下層から不成立のプロパティを検出していくことで、不成立の根本原因となるプロパティを早期に突き止めることができる。
【００６８】
また、修正対象アサーションの不成立回数に到達した場合は、その修正対象の木構造データからはこれ以上、不成立のプロパティが存在しないため、そのような木構造データについては検出処理の実行をスキップすることで、修正処理の高速化を図ることができる。
【００６９】
以上のことから、本実施の形態によれば、理解不足や誤解がある状態でアサーションが作成された場合であっても、修正すべきプロパティを自動的に突き止めることができ、そのようなプロパティに対し適切な修正処理を自動実行することができる。したがって、検証者が自ら仕様書を再分析して、または検証者が設計者とともに仕様書を再確認し、その上でアサーションを修正するといった作業負担が軽減し、アサーションの修正作業時間の短縮化を図ることができる。また、これにより、アサーションの修正作業の効率化を図ることができる。
【００７０】
なお、本実施の形態で説明した修正方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本修正プログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本修正プログラムは、インターネット等のネットワークを介して配布してもよい。
【符号の説明】
【００７１】
１００ 修正装置
１００１ 実行部
１００２ 取得部
１００３ 選択部
１００４ 分解部
１００５ 生成部
１００６ 検出部
１００７ 結合部
１００８ 算出部
１００９ 判断部
１０１０ 出力部
【技術分野】
【０００１】
本発明は、情報を修正する修正プログラム、修正装置、および修正方法に関する。
【背景技術】
【０００２】
従来、シミュレーション結果履歴として、不合格となったアサーション及び合格となったアサーションを特定するための「不合格が発生した回数」、「不合格が発生した時刻に関する情報」などを記憶する技術が開示されている。また、シミュレーションでエラーが発生した場合に、テストプログラムのどのパターンでエラーが発生したかを解析し、解析したエラー発生パターンを表示する技術も開示されている。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２００８−１５８６９６号公報
【特許文献２】特開２００２−１４９４４０号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
アサーションの作成元となる仕様書について、検証者が理解不足であったり誤解している場合、作成されたアサーションに誤りが存在する。このようなアサーションを用いて対象回路のシミュレーションを実行して、アサーションが不成立になった場合、アサーションが正しくて不成立になったかアサーションに誤りがあったために不成立になったかの判別がつかない。また、不成立の原因となるシミュレーション結果は、アサーションの内容により複数とおり出現することもある。
【０００５】
したがって、検証者が自ら仕様書を再分析して、または検証者が設計者とともに仕様書を再確認し、その上でアサーションを修正する必要がある。これにより、アサーションの修正作業に時間がかかる。
【０００６】
また、上述した従来技術では、アサーション自体が正しいものであるとの前提で処理をおこなっているため、仕様書の理解不足や誤解に基づくアサーションの誤りを特定することは困難である。
【０００７】
本発明の一側面では、アサーションの修正作業の効率化を図ることができる修正プログラム、修正装置、および修正方法を提供することを目的とする。
【課題を解決するための手段】
【０００８】
本発明の一側面として、修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解し、対象回路のシミュレーションを実行することにより、前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出し、検出された不成立になったプロパティに、不成立の原因要素を論理和で結合し、結合されたプロパティを出力する修正プログラム、修正装置、および修正方法が提案される。
【発明の効果】
【０００９】
本発明の一側面によれば、アサーションの修正作業の効率化を図ることができるという効果を奏する。
【図面の簡単な説明】
【００１０】
【図１】図１は、本実施の形態にかかるアサーション修正例を示す説明図である。
【図２】図２は、修正対象の絞込み例を示す説明図である。
【図３】図３は、シミュレーション結果２００の選択画面例を示す説明図である。
【図４】図４は、木構造データを示す説明図である。
【図５】図５は、修正対象アサーションから分解されたプロパティ群での対象回路ＤＵＴの再シミュレーション結果５００を示す説明図である。
【図６】図６は、プロパティ修正例を示す説明図（その１）である。
【図７】図７は、プロパティ修正例を示す説明図（その２）である。
【図８】図８は、プロパティ修正例を示す説明図（その３）である。
【図９】図９は、実施の形態にかかる修正装置１００のハードウェア構成例を示すブロック図である。
【図１０】図１０は、修正装置１００の機能的構成を示すブロック図である。
【図１１】図１１は、修正装置１００による修正処理手順を示すフローチャートである。
【図１２】図１２は、図１１に示した修正処理（ステップＳ１１０９）の詳細な処理手順例を示すフローチャートである。
【発明を実施するための形態】
【００１１】
以下に添付図面を参照して、この発明にかかる修正プログラム、修正装置、および修正方法の実施の形態を詳細に説明する。
【００１２】
本実施の形態では、対象回路のシミュレーションにより不成立（失敗）となったアサーションを修正対象とする。ここで、アサーションとは、対象回路の設計が満たすべき性質を記述した情報である。ＳＶＡ（Ｓｙｓｔｅｍ Ｖｅｒｉｌｏｇ Ａｓｓｅｒｔｉｏｎ）を例に挙げると、プロパティとして「Ａ＝＝Ｂ」が記述されている場合、変数／信号Ａが常に変数／信号Ｂと同じであることを確認すべきことを意味している。
【００１３】
また、プロパティとして「Ａ｜−＞Ｂ」が記述されている場合、イベントＡが発生した場合、イベントＢが発生することを確認すべきことを意味している。また、プロパティとして「Ａ＆＆Ｂ」が記述されている場合、ビット値Ａおよびビット値Ｂが常に「１」に設定されることを確認すべきことを意味している。
【００１４】
アサーションが成立していれば、対象回路は仕様書どおりに振舞っていることがわかる。一方、アサーションが不成立であれば、対象回路は仕様書どおりに動作していないことがわかる。ここで、検証者が対象回路の仕様書について理解不足であったり、誤解をしていた場合、アサーションが不成立になっても、仕様書にはない動作による不成立であるか仕様書どおりの動作であるにもかかわらずアサーションの誤りによる不成立であるかの判別がつかない。そこで、本実施の形態では、不成立のあったアサーションについて、不成立の原因となった要素（変数、信号、ビット値）を不成立のあったアサーションに対し論理和で追加する。
【００１５】
また、アサーション自体は、複雑な記述や冗長な記述となっている場合が多い。したがって、不成立となったアサーションのどの箇所を修正すべきか検証者が確認する必要がある。したがって、本実施の形態では、シミュレーションに先立って、アサーションを分解する。本実施の形態では、分解された記述を「プロパティ」と称す。プロパティは、上述した「Ａ＝＝Ｂ」、「Ａ｜−＞Ｂ」、「Ａ＆＆Ｂ」のような単純な式である。したがって、シミュレーションにおいて不成立となったプロパティに対し修正したり修正案を提示することで、修正作業の効率化を図る。
【００１６】
＜アサーション修正例＞
図１は、本実施の形態にかかるアサーション修正例を示す説明図である。図１において、アサーションＡ５は、対象回路ＤＵＴの設計情報１０１によるシミュレーションで不成立となったアサーションである。アサーションＡ５は、複数のプロパティｐ１〜ｐ４が論理和（｜｜）または論理積（＆＆）で結合された情報である。
【００１７】
したがって、修正装置１００は、アサーションＡ５を論理和および論理積の箇所を境界にして分解する。図１では、アサーションＡ５は、プロパティｐ１〜ｐ４に分解される。分解されたプロパティｐ１〜ｐ４は、アサーションＡ５の論理構造にしたがって木構造データＴ５となる。
【００１８】
プロパティｐ１〜ｐ４は、テストベンチ１０２に組み込まれ（図１では例としてｐ１）、対象回路ＤＵＴの設計情報１０１を用いた対象回路ＤＵＴのシミュレーションにより、成立、不成立が判断される。たとえば、クロックの立ち上がり時に、レジスタＲｂ，Ｒｃのビット値Ｂ，Ｃが「０」、レジスタＲｘのビット値Ｘが「１」になった場合、プロパティｐ１は不成立となる。
【００１９】
この場合、修正装置１００は、プロパティｐ１に、「｜｜Ｘ」を追加することで、プロパティｐ１を修正する。したがって、修正後にシミュレーションを実行すると、クロックの立ち上がり時に、レジスタＲｂ，Ｒｃのビット値Ｂ，Ｃが「０」、レジスタＲｘのビット値Ｘが「１」になった場合、修正プロパティＰ１は成立することになる。
【００２０】
＜修正対象の絞込み例＞
図２は、修正対象の絞込み例を示す説明図である。図２では、図１のアサーションの分解に先立って、修正対象のアサーションを絞り込む。これにより、誤りが潜んでいる可能性が高いアサーションを優先的に抽出することができる。
【００２１】
具体的には、アサーション群が組み込まれたテストベンチ１０２と対象回路ＤＵＴの設計情報１０１とを用いた対象回路ＤＵＴのシミュレーションにより、修正装置１００は、シミュレーション結果２００を得る。シミュレーション結果２００では、アサーションごとにアサーションＩＤと不成立回数が記憶されている。アサーションＩＤは、アサーションを特定する識別コードである。本例では、説明の都合上、アサーションに割り当てた符号を識別コードとしている。
【００２２】
不成立回数とは、シミュレーション時にアサーションが成立しなかった回数であり、シミュレーション中に計数される。この不成立回数には、不成立の原因が複数とおりある場合、それらの不成立回数が混在する。たとえば、アサーションＡ５の不成立回数は２０であるが、プロパティｐ１〜ｐ４での不成立回数の合計が２０回であることを意味しており、内訳はプロパティごとに異なる。
【００２３】
たとえば、プロパティｐ１が１３回、プロパティｐ２が７回、プロパティｐ３，ｐ４が０回である場合、プロパティｐ３，ｐ４については修正する必要がないことがわかる。このように、アサーションを分解することで、修正すべきプロパティと修正すべきでないプロパティを特定することができる。
【００２４】
図３は、シミュレーション結果２００の選択画面例を示す説明図である。図３では、シミュレーション結果２００が選択画面３００に表示されている。具体的には、たとえば、アサーションごとに、アサーションＩＤと不成立回数とチェックボックスとが表示されている。不成立回数が多いアサーションほど誤りが潜んでいる可能性が高い。したがって、検証者は、マウスなどの入力装置を操作して、修正したいアサーションのチェックボックス３０１にチェックを入れて、確認ボタン３０２を押下することで、修正対象アサーションが決定される。
【００２５】
図３の場合、アサーションＡ５，Ａ７，Ａ４，Ａ２が修正対象アサーションとなる。なお、図２および図３では、不成立回数を記憶、表示させているが、不成立確率（＝不成立回数／（成立回数＋不成立回数））を記憶、表示させることとしてもよい。
【００２６】
図４は、木構造データを示す説明図である。木構造データは、図１に示したように、アサーションをその論理構造で分解し、関連しあうプロパティを連結した構造体である。図４において、○は木構造データの節点であり、プロパティを示す。○内の符号でプロパティを示している。木構造データは修正対象アサーションごとに生成される。各木構造データの最上位階層を第１階層とし、階層が下がるごとに階層番号ｒが増加する。図４の場合は、アサーションＡ７の第５階層が最下位階層となる。
【００２７】
図５は、修正対象アサーションから分解されたプロパティ群での対象回路ＤＵＴの再シミュレーション結果５００を示す説明図である。図５では、プロパティごとに、プロパティＩＤ、不成立回数、および不成立原因要素が記憶される。プロパティＩＤは、プロパティを特定する識別コードである。本例では、説明の都合上、プロパティに割り当てた符号を識別コードとしている。不成立回数とは、シミュレーション時にプロパティが成立しなかった回数であり、再シミュレーション中に計数される。
【００２８】
不成立原因要素とは、プロパティが不成立となった原因を示す要素である。たとえば、プロパティｐ１の不成立原因要素は「Ｘ」となっている。すなわち、レジスタＲｂ，Ｒｃのビット値ＢまたはＣの少なくともいずれか一方が「１」になるべきところ、いずれも「０」で、レジスタＲＸのビット値Ｘが「Ｘ＝１」になったために、不成立になったことを示している。
【００２９】
また、プロパティｐ２の不成立原因要素は「Ｅ＝＝３」となっている。すなわち、プロパティｐ２ではＤ＝１の１サイクル後にＥ＝＝２となるべきところ、「Ｅ＝＝３」になったために、不成立になったことを示している。
【００３０】
また、プロパティｐ５の不成立原因要素は「Ｇ＝＝Ｊ」となっている。すなわち、プロパティｐ５では、変数／信号Ｇが常に変数／信号Ｈと同じであるべきところ、「Ｇ＝＝Ｊ」になったために、不成立になったことを示している。
【００３１】
＜プロパティ修正例＞
図６〜図８は、プロパティ修正例を示す説明図である。図６は、プロパティｐ２の修正例を示している。プロパティｐ２では、Ｄ＝１の１サイクル後にＥ＝＝２となるべきところ、「Ｅ＝＝３」になったために、不成立になっている。したがって、修正装置１００は、プロパティｐ２に不成立原因要素である「Ｅ＝＝３」を論理和で結合する。これにより、プロパティｐ２が修正プロパティＰ２となる。したがって、次回のシミュレーションで、Ｄ＝＝１の１サイクル後は、「Ｅ＝＝２」または「Ｅ＝＝３」のいずれかになれば、修正プロパティＰ２が成立することになる。
【００３２】
図７は、プロパティｐ１の修正例を示している。プロパティｐ１では、レジスタＲｂ，Ｒｃのビット値ＢまたはＣの少なくともいずれか一方が「１」になるべきところ、いずれも「０」で、レジスタＲＸのビット値ｘが「Ｘ＝１」になったために、不成立になっている。したがって、修正装置１００は、プロパティｐ１に不成立原因要素である「Ｘ」を論理和で結合する。これにより、プロパティｐ１が修正プロパティＰ１となる。したがって、次回のシミュレーションで、レジスタＲｂ，Ｒｃ，Ｒｘのビット値Ｂ，ＣまたはＸの少なくともいずれか一つが「１」になれば、修正プロパティＰ１が成立することになる。
【００３３】
図８は、プロパティｐ５の修正例を示している。プロパティｐ５では、変数／信号Ｇが常に変数／信号Ｈと同じであるべきところ、「Ｇ＝＝Ｊ」になったために、不成立になっている。したがって、修正装置１００は、プロパティｐ５に不成立原因要素である「Ｇ＝＝Ｊ」を論理和で結合する。これにより、プロパティｐ５が修正プロパティＰ５となる。したがって、次回のシミュレーションで、「Ｇ＝＝Ｈ」または「Ｇ＝＝Ｊ」のいずれかになれば、修正プロパティＰ５が成立することになる。
【００３４】
＜修正装置１００のハードウェア構成例＞
図９は、実施の形態にかかる修正装置１００のハードウェア構成例を示すブロック図である。図９において、修正装置１００は、ＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）９０１と、ＲＯＭ（Ｒｅａｄ‐Ｏｎｌｙ Ｍｅｍｏｒｙ）９０２と、ＲＡＭ（Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）９０３と、磁気ディスクドライブ９０４と、磁気ディスク９０５と、光ディスクドライブ９０６と、光ディスク９０７と、ディスプレイ９０８と、Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）９０９と、キーボード９１０と、マウス９１１と、スキャナ９１２と、プリンタ９１３と、を備えている。また、各構成部はバス９００によってそれぞれ接続されている。
【００３５】
ここで、ＣＰＵ９０１は、修正装置１００の全体の制御を司る。ＲＯＭ９０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ９０３は、ＣＰＵ９０１のワークエリアとして使用される。磁気ディスクドライブ９０４は、ＣＰＵ９０１の制御にしたがって磁気ディスク９０５に対するデータのリード／ライトを制御する。磁気ディスク９０５は、磁気ディスクドライブ９０４の制御で書き込まれたデータを記憶する。
【００３６】
光ディスクドライブ９０６は、ＣＰＵ９０１の制御にしたがって光ディスク９０７に対するデータのリード／ライトを制御する。光ディスク９０７は、光ディスクドライブ９０６の制御で書き込まれたデータを記憶したり、光ディスク９０７に記憶されたデータをコンピュータに読み取らせたりする。
【００３７】
ディスプレイ９０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ９０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００３８】
インターフェース（以下、「Ｉ／Ｆ」と略する。）９０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ Ａｒｅａ Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ Ａｒｅａ Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク９１４に接続され、このネットワーク９１４を介して他の装置に接続される。そして、Ｉ／Ｆ９０９は、ネットワーク９１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ９０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００３９】
キーボード９１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス９１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００４０】
スキャナ９１２は、画像を光学的に読み取り、修正装置１００内に画像データを取り込む。なお、スキャナ９１２は、ＯＣＲ（Ｏｐｔｉｃａｌ Ｃｈａｒａｃｔｅｒ Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ９１３は、画像データや文書データを印刷する。プリンタ９１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００４１】
＜修正装置１００の機能的構成例＞
図１０は、修正装置１００の機能的構成を示すブロック図である。修正装置１００は、実行部１００１と、取得部１００２と、選択部１００３と、分解部１００４と、生成部１００５と、検出部１００６と、結合部１００７と、算出部１００８と、判断部１００９と、出力部１０１０と、を備えている。実行部１００１〜出力部１０１０は、は、具体的には、たとえば、図９に示したＲＯＭ９０２、ＲＡＭ９０３、磁気ディスク９０５、光ディスク９０７などの記憶装置に記憶されたプログラムをＣＰＵ９０１に実行させることにより、または、Ｉ／Ｆ９０９により、その機能を実現する。
【００４２】
実行部１００１は、対象回路ＤＵＴの設計情報１０１によるシミュレーションを実行する。具体的には、たとえば、図２に示したように、実行部１００１は、シミュレーションを実行する。また、実行部１００１は、シミュレーション中に、アサーションが成立（成功）するか不成立になる（失敗）かを判断する。不成立の場合は、アサーションごとに不成立回数を計数して、図２に示したようにシミュレーション結果２００として記憶装置に記憶する。
【００４３】
取得部１００２は、対象回路ＤＵＴのシミュレーションを実行することによりアサーションごとの不成立回数を取得する。具体的には、たとえば、図２に示したシミュレーション結果２００が実行部１００１により記憶装置に記憶されるため、取得部１００２は、記憶装置のシミュレーション結果２００の中からアサーションごとの不成立回数を読み出す。
【００４４】
選択部１００３は、取得部１００２によって取得された不成立回数に基づいてアサーション群の中から修正対象アサーションを選択する。具体的には、たとえば、取得部１００２によって取得された不成立回数に基づいて図３に示した選択画面３００が表示される。したがって、検証者は、マウス９１１などの入力装置を操作して修正したいアサーションのチェックボックス３０１にチェックを入れ、確認ボタン３０２を押下する。これにより、選択部１００３は、チェックボックス３０１にチェックが入れられたアサーションを修正対象アサーションであると認識する。
【００４５】
分解部１００４は、修正対象アサーションをアサーションの論理構造に基づいて分解する。分解対象となる修正対象アサーションは、検証者が任意に決めてもよく、また、選択部１００３によって選択されたアサーションを修正対象アサーションとしてもよい。分解部１００４では、図１に示したように、論理和または論理積で結合されている式をプロパティとして抽出する。抽出されたプロパティ群は修正対象アサーションごとに記憶装置に記憶される。
【００４６】
生成部１００５は、分解部１００４によって分解されたプロパティ群の木構造データを生成する。具体的には、たとえば、生成部１００５は、修正対象アサーションごとに得られたプロパティ群内の包含関係により木構造データを生成する。たとえば、プロパティｐ４にはプロパティｐ２，ｐ３が包含されているため、プロパティｐ２，ｐ３は、プロパティｐ４の下位階層のプロパティとして連結される。プロパティｐ３にはプロパティｐ１が包含されているため、プロパティｐ１は、プロパティｐ３の下位階層のプロパティとして連結される。これにより、図４に示したような木構造データが修正対象プロパティごとに生成されることになる。
【００４７】
また、実行部１００１は、図１に示したように、分解されたプロパティ群を用いて対象回路ＤＵＴのシミュレーション（再シミュレーション）を実行する。再シミュレーションでは、プロパティごとに不成立回数を計数し、不成立原因要素を検出する。これにより、図５に示したような再シミュレーション結果５００が得られる。再シミュレーション結果５００は、記憶装置に記憶される。
【００４８】
検出部１００６は、対象回路ＤＵＴのシミュレーションを実行することにより、分解部１００４によって修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出する。具体的には、たとえば、検出部１００６は、再シミュレーション結果５００の中で所定回数（たとえば１回）以上不成立となったプロパティを修正対象プロパティとして検出する。
【００４９】
また、検出部１００６は、生成部１００５によって生成された木構造データを構成するプロパティ群のうち最下層のプロパティから検出する。たとえば、図４の例では、第５階層のプロパティｐ５，ｐ６を検出し、つぎに、第４階層のプロパティｐ７，ｐ１１を検出し、つぎに、第３階層のプロパティｐ１、ｐ８、ｐ１２〜ｐ１４を検出する。このように、段階的に階層を上げていき、検出部１００６は、最終的に第１階層のプロパティｐ４、ｐ１０、ｐ１７，１８を検出することになる。また、検出部１００６は、再シミュレーション結果５００から修正対象プロパティの不成立原因要素を検出する。
【００５０】
結合部１００７は、検出部１００６によって検出された不成立になったプロパティに、不成立の原因要素を論理和で結合する。結合部１００７は、具体的には、たとえば、図６〜図８に示したように、論理和で結合する。
【００５１】
算出部１００８は、修正対象アサーションごとに、結合部１００７によって結合する都度、結合されたプロパティについての結合前の不成立回数を累積する。たとえば、修正対象アサーションＡ５のプロパティｐ１〜ｐ４を例に挙げると、修正対象アサーションＡ５の不成立回数は２０回（図２を参照）であり、プロパティｐ１の不成立回数は１３回、プロパティｐ２の不成立回数は７回、プロパティｐ３，ｐ４の不成立回数はともに０回である（図５を参照）。
【００５２】
まず、累積不成立回数の初期値は０である。検出部１００６は、最下層である第５階層から順次修正対象プロパティを検出するため、修正対象アサーションＡ５の木構造データＴ５については、第３階層のプロパティｐ１が最初に検出されて、結合部１００７により結合が行われる。このとき、プロパティｐ１の不成立回数は１３回であるため、累積不成立回数に累積することで、０＋１３＝１３回となる。つぎに、第２階層のプロパティｐ２が検出されて、結合部１００７により結合が行われる。このとき、プロパティｐ２の不成立回数は７回であるため、累積不成立回数に累積することで、１３＋７＝２０回となる。
【００５３】
判断部１００９は、修正対象アサーションごとに、算出部１００８によって累積された不成立回数が、修正対象アサーションの不成立回数に到達したか否かを判断する。具体的には、累積される都度、判断部１００９は、修正対象アサーションの不成立回数に到達したか否かを判断する。
【００５４】
たとえば、上記の例で、第２階層のプロパティｐ２が検出されて、累積不成立回数が、１３＋７＝２０回となった場合、修正対象アサーションＡ５の不成立回数２０回に到達したと判断する。この場合、検出部１００６は、木構造データＴ５については、これ以上、不成立のプロパティｐ３，ｐ４の検出はおこなわない。
【００５５】
すなわち、検出処理を実行しても、不成立のプロパティは得られないため、木構造データＴ５を検出対象から除外する。たとえば、検出不可フラグを設定したり、木構造データＴ５を消去したりする。これにより、修正処理の高速化を図ることができる。
【００５６】
出力部１０１０は、結合部１００７によって結合されたプロパティを出力する。具体的には、たとえば、出力部１０１０は、結合されたプロパティ、すなわち、修正済みのプロパティを出力する。また、修正する必要がなかったプロパティも出力する。これらのプロパティをまとめて修正プロパティ群と称す。修正プロパティ群は、ディスプレイ９０８に出力することで、表示される。また、プリンタ９１３に出力されることで印刷される。また、Ｉ／Ｆ９０９に出力されることで、外部装置に送信される。また、記憶装置に出力されることで、修正プロパティ群が保存される。
【００５７】
＜修正処理手順＞
図１１は、修正装置１００による修正処理手順を示すフローチャートである。まず、修正装置１００は、図２に示したようなシミュレーション結果２００を取得して（ステップＳ１１０１）、不成立回数の降順にアサーションを並び替える（ステップＳ１１０２）。そして、修正装置１００は、図３に示したような、並び替え後のアサーションを示す選択画面３００をディスプレイ９０８に表示する（ステップＳ１１０３）。
【００５８】
修正装置１００は、選択部１００３により選択入力があった場合（ステップＳ１１０４：Ｙｅｓ）、選択アサーションＩＤを保持して（ステップＳ１１０５）、ステップＳ１１０６に移行する。一方、選択入力がない場合（ステップＳ１１０４：Ｎｏ）、ステップＳ１１０６に移行する。
【００５９】
ステップＳ１１０６において、修正装置１００は、選択画面３００の確認ボタン３０２の選択入力による確定選択があったか否かを判断する（ステップＳ１１０６）。確定選択がない場合（ステップＳ１１０６：Ｎｏ）、ステップＳ１１０４に戻る。一方、確定選択があった場合（ステップＳ１１０６：Ｙｅｓ）、修正装置１００は、選択アサーションＩＤがあるか否かを判断する（ステップＳ１１０７）。
【００６０】
選択アサーションＩＤがない場合（ステップＳ１１０７：Ｎｏ）、アサーションを１つも選択せずに確定選択をしたこととなり、一連の処理を終了する。一方、選択アサーションＩＤがある場合（ステップＳ１１０７：Ｙｅｓ）、選択アサーションＩＤを手がかりにして、シミュレーション結果２００から選択アサーションを抽出する（ステップＳ１１０８）。そして、抽出された選択アサーションは修正対象アサーションになるため、修正装置１００は、修正対象アサーションについて修正処理を実行する（ステップＳ１１０９）。修正処理（ステップＳ１１０９）の詳細は図１２で後述する。
【００６１】
修正処理（ステップＳ１１０９）後、修正装置１００は、出力部１０１０により、修正プロパティ群を出力する（ステップＳ１１１０）ことで、一連の処理を終了する。なお、修正プロパティ群については、検証者がマウス９１１やキーボード９１０などの入力装置を操作することで、適宜修正をおこなってもよい。
【００６２】
図１２は、図１１に示した修正処理（ステップＳ１１０９）の詳細な処理手順例を示すフローチャートである。まず、修正装置１００は、未選択の修正対象アサーションがあるか否かを判断する（ステップＳ１２０１）。未選択の修正対象アサーションがある場合（ステップＳ１２０１：Ｙｅｓ）、修正装置１００は、選択部１００３により未選択の修正対象アサーションを選択し（ステップＳ１２０２）、分解部１００４により、修正対象アサーションを分解する（ステップＳ１２０３）。そして、修正装置１００は、生成部１００５により、分解されたプロパティ群で修正対象アサーションの木構造データを生成して（ステップＳ１２０４）、ステップＳ１２０１に戻る。
【００６３】
また、ステップＳ１２０１において、未選択の修正対象アサーションがない場合（ステップＳ１２０１：Ｎｏ）、修正装置１００は、階層番号ｒをｒ＝Ｒに設定する（ステップＳ１２０５）。Ｒは、生成された木構造データ群の最下層である。図４の例ではＲ＝５となる。つぎに、修正装置１００は、実行部１００１により、プロパティ群（木構造データ群）を用いて対象回路ＤＵＴの再シミュレーションを実行する（ステップＳ１２０６）。
【００６４】
そして、修正装置１００は、検出部１００６により、木構造データ群の第ｒ階層のプロパティから不成立のプロパティを検出する（ステップＳ１２０７）。つぎに、修正装置１００は、図６〜図８に示したように、結合部１００７により、不成立のプロパティの不成立原因要素を、論理和で不成立のプロパティに結合する（ステップＳ１２０８）。
【００６５】
そして、修正装置１００は、算出部１００８により修正済みプロパティの不成立回数を修正対象アサーションごとに累積計算する（ステップＳ１２０９）。このあと、修正装置１００は、判断部１００９により、修正対象アサーションごとに、修正対象アサーションの不成立回数に到達したか否かを判断する（ステップＳ１２１０）。到達していない修正対象アサーションについては（ステップＳ１２１０：Ｎｏ）、ステップＳ１２１２に移行する。一方、到達した修正対象アサーションについては（ステップＳ１２１０：Ｙｅｓ）、到達した修正対象アサーションの木構造データを修正対象外に設定し（ステップＳ１２１１）、ステップＳ１２１２に移行する。これにより、以降の修正処理の高速化を図ることができる。
【００６６】
ステップＳ１２１２では、修正装置１００は、階層番号ｒをデクリメントし（ステップＳ１２１２）、ｒ＝０であるか否かを判断する（ステップＳ１２１３）。ｒ＝０でない場合（ステップＳ１２１３：Ｎｏ）、ステップＳ１２０７に戻る。一方、ｒ＝０である場合（ステップＳ１２１３：Ｙｅｓ）、修正処理（ステップＳ１１０９）を終了し、ステップＳ１１１０に移行する。なお、上述した修正処理（ステップＳ１１０９）においては、ステップＳ１２０９〜Ｓ１２１１を省略してもよい。
【００６７】
このように、本実施の形態によれば、不成立となったアサーションをプロパティ群に分解し、不成立のプロパティごとに、不成立原因要素を論理和で結合するため、修正処理の自動化を図ることができる。また、アサーションではなくプロパティ単位で修正処理をおこなうため、修正箇所を人手で探さずに自動で修正箇所を突き止めることができる。したがって、修正処理の高速化を図ることができる。また、木構造データの最下層から不成立のプロパティを検出していくことで、不成立の根本原因となるプロパティを早期に突き止めることができる。
【００６８】
また、修正対象アサーションの不成立回数に到達した場合は、その修正対象の木構造データからはこれ以上、不成立のプロパティが存在しないため、そのような木構造データについては検出処理の実行をスキップすることで、修正処理の高速化を図ることができる。
【００６９】
以上のことから、本実施の形態によれば、理解不足や誤解がある状態でアサーションが作成された場合であっても、修正すべきプロパティを自動的に突き止めることができ、そのようなプロパティに対し適切な修正処理を自動実行することができる。したがって、検証者が自ら仕様書を再分析して、または検証者が設計者とともに仕様書を再確認し、その上でアサーションを修正するといった作業負担が軽減し、アサーションの修正作業時間の短縮化を図ることができる。また、これにより、アサーションの修正作業の効率化を図ることができる。
【００７０】
なお、本実施の形態で説明した修正方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本修正プログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本修正プログラムは、インターネット等のネットワークを介して配布してもよい。
【符号の説明】
【００７１】
１００ 修正装置
１００１ 実行部
１００２ 取得部
１００３ 選択部
１００４ 分解部
１００５ 生成部
１００６ 検出部
１００７ 結合部
１００８ 算出部
１００９ 判断部
１０１０ 出力部
【特許請求の範囲】
【請求項１】
修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解し、
対象回路のシミュレーションを実行することにより、前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出し、
検出された不成立になったプロパティに、不成立の原因要素を論理和で結合し、
結合されたプロパティを出力する、
処理をコンピュータに実行させることを特徴とする修正プログラム。
【請求項２】
前記プロパティ群の木構造データを生成する処理を前記コンピュータに実行させ、
前記検出する処理では、
前記生成する処理によって生成された木構造データを構成するプロパティ群のうち最下層のプロパティから検出することを特徴とする請求項１に記載の修正プログラム。
【請求項３】
前記対象回路のシミュレーションを実行することによりアサーションごとの不成立回数を取得し、
取得された不成立回数に基づいてアサーション群の中から前記修正対象アサーションを選択する、処理を前記コンピュータに実行させ、
前記分解する処理では、
前記選択する処理によって選択された修正対象アサーションを前記アサーションの論理構造に基づいて分解することを特徴とする請求項１または２に記載の修正プログラム。
【請求項４】
修正対象アサーションごとに、前記結合する処理によって結合する都度、結合されたプロパティについての結合前の不成立回数を累積し、
前記修正対象アサーションごとに、累積された不成立回数が、修正対象アサーションの不成立回数に到達したか否かを判断する、処理を前記コンピュータに実行させ、
前記検出する処理では、
前記判断する処理によって到達したと判断された修正対象アサーションの木構造データから検出しないことを特徴とする請求項３に記載の修正プログラム。
【請求項５】
修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解する分解手段と、
対象回路のシミュレーションを実行することにより、前記分解手段によって前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出する検出手段と、
前記検出手段によって検出された不成立になったプロパティに、不成立の原因要素を論理和で結合する結合手段と、
前記結合手段によって結合されたプロパティを出力する出力手段と、
を備えることを特徴とする修正装置。
【請求項６】
修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解し、
対象回路のシミュレーションを実行することにより、前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出し、
検出された不成立になったプロパティに、不成立の原因要素を論理和で結合し、
結合されたプロパティを出力する、
処理をコンピュータが実行することを特徴とする修正方法。
【請求項１】
修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解し、
対象回路のシミュレーションを実行することにより、前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出し、
検出された不成立になったプロパティに、不成立の原因要素を論理和で結合し、
結合されたプロパティを出力する、
処理をコンピュータに実行させることを特徴とする修正プログラム。
【請求項２】
前記プロパティ群の木構造データを生成する処理を前記コンピュータに実行させ、
前記検出する処理では、
前記生成する処理によって生成された木構造データを構成するプロパティ群のうち最下層のプロパティから検出することを特徴とする請求項１に記載の修正プログラム。
【請求項３】
前記対象回路のシミュレーションを実行することによりアサーションごとの不成立回数を取得し、
取得された不成立回数に基づいてアサーション群の中から前記修正対象アサーションを選択する、処理を前記コンピュータに実行させ、
前記分解する処理では、
前記選択する処理によって選択された修正対象アサーションを前記アサーションの論理構造に基づいて分解することを特徴とする請求項１または２に記載の修正プログラム。
【請求項４】
修正対象アサーションごとに、前記結合する処理によって結合する都度、結合されたプロパティについての結合前の不成立回数を累積し、
前記修正対象アサーションごとに、累積された不成立回数が、修正対象アサーションの不成立回数に到達したか否かを判断する、処理を前記コンピュータに実行させ、
前記検出する処理では、
前記判断する処理によって到達したと判断された修正対象アサーションの木構造データから検出しないことを特徴とする請求項３に記載の修正プログラム。
【請求項５】
修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解する分解手段と、
対象回路のシミュレーションを実行することにより、前記分解手段によって前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出する検出手段と、
前記検出手段によって検出された不成立になったプロパティに、不成立の原因要素を論理和で結合する結合手段と、
前記結合手段によって結合されたプロパティを出力する出力手段と、
を備えることを特徴とする修正装置。
【請求項６】
修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解し、
対象回路のシミュレーションを実行することにより、前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出し、
検出された不成立になったプロパティに、不成立の原因要素を論理和で結合し、
結合されたプロパティを出力する、
処理をコンピュータが実行することを特徴とする修正方法。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【公開番号】特開２０１３−４７９１５（Ｐ２０１３−４７９１５Ａ）
【公開日】平成２５年３月７日（２０１３．３．７）
【国際特許分類】
【出願番号】特願２０１１−１８６５４７（Ｐ２０１１−１８６５４７）
【出願日】平成２３年８月２９日（２０１１．８．２９）
【出願人】（０００００５２２３）富士通株式会社 (25,993)
【Ｆターム（参考）】
【公開日】平成２５年３月７日（２０１３．３．７）
【国際特許分類】
【出願日】平成２３年８月２９日（２０１１．８．２９）
【出願人】（０００００５２２３）富士通株式会社 (25,993)
【Ｆターム（参考）】
[ Back to top ]