(57)【要約】【課題】コンピュータプログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の検証を簡便ならしめることができる回路記述の抽象化装置及び検証装置、回路記述の抽象化プログラム及び検証プログラム、並びに回路記述の抽象化方法及び検証方法を提供する。【解決手段】回路記述の仕様データ２４が示す論理モデル内に含まれる各計算処理ユニットに対して、予め設定した閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定し、判定結果が肯定判定である場合、前記閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットの一覧を、入力装置１２からの入力操作に基づき選択可能な態様で出力装置１３に出力する。そして、論理モデル内にて、検証不能計算処理ユニットであると判定された計算処理ユニットを、検証可能計算処理ユニットの一覧から選択した計算処理ユニットに置換する。【選択図】図１
2010079433.tif 000002
【特許請求の範囲】
【請求項１】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの抽象化の処理手順を制御する制御手段とを備えた回路記述の抽象化装置であって、
前記制御手段は、
予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶手段と、
前記論理モデル内に含まれる少なくとも一つの計算処理ユニットについて、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定手段と、
該ユニット判定手段の判定結果が肯定判定である場合に、前記ユニット記憶手段に記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力手段と、
前記検証不能計算処理ユニットを前記ユニット出力手段が出力した前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換手段と
を備えたことを特徴とする回路記述の抽象化装置。
【請求項２】
前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを特徴とする請求項１に記載の回路記述の抽象化装置。
【請求項３】
前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを特徴とする請求項１に記載の回路記述の抽象化装置。
【請求項４】
前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータを前記検証可能計算処理ユニットの入力データとして入力した場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項１〜請求項３のうち何れか一項に記載の回路記述の抽象化装置。
【請求項５】
前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項１〜請求項３のうち何れか一項に記載の回路記述の抽象化装置。
【請求項６】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの検証の処理手順を制御する制御手段とを備えた回路記述の検証装置であって、
前記制御手段は、
予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶手段と、
前記論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定手段と、
該ユニット判定手段の判定結果が肯定判定である場合に、前記ユニット記憶手段に記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力手段と、
前記検証不能計算処理ユニットを前記ユニット出力手段が出力した前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換手段と
該ユニット置換手段により計算処理ユニットが置換された前記論理モデルを検証対象にした検証作業を実行する検証手段と
を備えたことを特徴とする回路記述の検証装置。
【請求項７】
前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを特徴とする請求項６に記載の回路記述の検証装置。
【請求項８】
前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを特徴とする請求項６に記載の回路記述の検証装置。
【請求項９】
前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータを前記検証可能計算処理ユニットの入力データとして入力した場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項６〜請求項８のうち何れか一項に記載の回路記述の検証装置。
【請求項１０】
前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項６〜請求項８のうち何れか一項に記載の回路記述の検証装置。
【請求項１１】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの抽象化の処理手順を制御する制御手段とを備えた回路記述の抽象化装置を稼動させるために用いられる回路記述の抽象化プログラムであって、
前記制御手段を、
予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶手段、
前記論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定手段、
該ユニット判定手段の判定結果が肯定判定である場合に、前記ユニット記憶手段に記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力手段、及び、
前記検証不能計算処理ユニットを前記ユニット出力手段が出力した前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換手段
として機能させることを特徴とする回路記述の抽象化プログラム。
【請求項１２】
前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを特徴とする請求項１１に記載の回路記述の抽象化プログラム。
【請求項１３】
前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを特徴とする請求項１１に記載の回路記述の抽象化プログラム。
【請求項１４】
前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータが前記検証可能計算処理ユニットの入力データとして入力された場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力させる計算処理ユニットであることを特徴とする請求項１１〜請求項１３のうち何れか一項に記載の回路記述の抽象化プログラム。
【請求項１５】
前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項１１〜請求項１３のうち何れか一項に記載の回路記述の抽象化プログラム。
【請求項１６】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの検証の処理手順を制御する制御手段とを備えた回路記述の検証装置を稼動させるために用いられる回路記述の検証プログラムであって、
前記制御手段を、
予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶手段、
前記論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定手段、
該ユニット判定手段の判定結果が肯定判定である場合に、前記ユニット記憶手段に記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力手段、
前記検証不能計算処理ユニットを前記ユニット出力手段が出力した前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換手段、及び、
該ユニット置換手段により計算処理ユニットが置換された前記論理モデルを検証対象にした検証作業を実行する検証手段
として機能させることを特徴とする回路記述の検証プログラム。
【請求項１７】
前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを特徴とする請求項１６に記載の回路記述の検証プログラム。
【請求項１８】
前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを特徴とする請求項１６に記載の回路記述の検証プログラム。
【請求項１９】
前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータが前記検証可能計算処理ユニットの入力データとして入力された場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項１６〜請求項１８のうち何れか一項に記載の回路記述の検証プログラム。
【請求項２０】
前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項１６〜請求項１８のうち何れか一項に記載の回路記述の検証プログラム。
【請求項２１】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の抽象化方法であって、
予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶段階と、
前記回路記述が示す論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定段階と、
該ユニット判定段階の判定結果が肯定判定である場合に、前記ユニット記憶段階にて記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力段階と、
前記検証不能計算処理ユニットを前記ユニット出力段階で出力された前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された前記検証可能計算処理ユニットに置換するユニット置換段階と
を備えたことを特徴とする回路記述の抽象化方法。
【請求項２２】
前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを特徴とする請求項２１に記載の回路記述の抽象化方法。
【請求項２３】
前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを特徴とする請求項２１に記載の回路記述の抽象化方法。
【請求項２４】
前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータが前記検証可能計算処理ユニットの入力データとして入力された場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項２１〜請求項２３のうち何れか一項に記載の回路記述の抽象化方法。
【請求項２５】
前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項２１〜請求項２３のうち何れか一項に記載の回路記述の抽象化方法。
【請求項２６】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の検証方法であって、
予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶段階と、
前記回路記述が示す論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定段階と、
該ユニット判定段階の判定結果が肯定判定である場合に、前記ユニット記憶段階にて記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力段階と、
前記検証不能計算処理ユニットを前記ユニット出力段階で出力された前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換段階と、
該ユニット置換段階にて計算処理ユニットが置換された前記論理モデルを検証対象にした検証作業を実行する検証段階と
を備えたことを特徴とする回路記述の検証方法。
【請求項２７】
前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを特徴とする請求項２６に記載の回路記述の検証方法。
【請求項２８】
前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを特徴とする請求項２６に記載の回路記述の検証方法。
【請求項２９】
前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータが前記検証可能計算処理ユニットの入力データとして入力された場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項２６〜請求項２８のうち何れか一項に記載の回路記述の検証方法。
【請求項３０】
前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを特徴とする請求項２６〜請求項２８のうち何れか一項に記載の回路記述の検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータプログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の抽象化装置及び検証装置、回路記述の抽象化プログラム及び検証プログラム、並びに回路記述の抽象化方法及び検証方法に関する。
【背景技術】
【０００２】
従来、設計したコンピュータプログラムが設計者の意図した設計思想どおりのふるまいをするか否かを検証するための技術として、形式的手法を用いた検証装置が広く知られている（例えば、特許文献１）。この検証装置では、例えばＣ、Ｃ＋＋、ＦＯＲＴＲＡＮ等のプログラム言語を用いて記述されたプログラムの記述内容を先ず既存のモデリング変換ソフト（Ｓｉｍｕｌｉｎｋ、Ｓｃａｄｅ等）を用いて形式的仕様記述言語による回路記述に変換するようにしている。そして、同回路記述で示される論理モデルについて数学的に検証を行うことで、形式的仕様の回路記述に変換されたプログラム内容の設計の正しさを証明することが可能となっている。
【特許文献１】特許第３６６００９７号公報
【発明の開示】
【発明が解決しようとする課題】
【０００３】
しかしながら、回路記述内に非線形の計算処理（例えば、二次以上の多次関数）を実行する計算処理ユニットが含まれる場合には、回路記述で示される論理モデルの正しさを数学的に証明することができず、形式的手法を用いた検証を適用することができないという問題があった。
【０００４】
また、回路記述内に過去の出力データを入力データとして再帰的に利用する計算処理を実行する計算処理ユニットが含まれる場合には、過去の出力データを読み出す際に、同計算処理ユニット内の計算処理を繰り返し実行することで過大な処理負荷を生じるため、形式的手法を用いた検証に膨大な時間を要するという問題があった。
【０００５】
本発明は、このような事情に鑑みてなされたものであり、その目的は、形式的手法を用いた検証に適さない計算処理ユニットを含む回路記述の検証を簡便ならしめることができる回路記述の抽象化装置及び検証装置、回路記述の抽象化プログラム及び検証プログラム、並びに回路記述の抽象化方法及び検証方法を提供することにある。
【課題を解決するための手段】
【０００６】
上記目的を達成するために、請求項１に記載の回路記述の抽象化装置は、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの抽象化の処理手順を制御する制御手段とを備えた回路記述の抽象化装置であって、前記制御手段は、予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶手段と、前記論理モデル内に含まれる少なくとも一つの計算処理ユニットについて、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定手段と、該ユニット判定手段の判定結果が肯定判定である場合に、前記ユニット記憶手段に記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力手段と、前記検証不能計算処理ユニットを前記ユニット出力手段が出力した前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換手段とを備えたことを要旨とする。
【０００７】
上記構成によれば、回路記述内に検証不能計算処理ユニットが含まれる場合には、該検証不能計算処理ユニットと置換可能な検証可能計算処理ユニットが選択可能に出力され、その出力結果の中から選択された検証可能計算処理ユニットに検証不能計算処理ユニットが置換される。そのため、検証可能計算処理ユニットを手入力する場合と比較して、回路記述の形式的仕様を、形式的手法を用いた検証に好適に適用できる仕様態様に簡便に変換することができる。したがって、回路記述が形式的手法を用いた検証に適さない検証不能計算処理ユニットを含んで構成される場合であっても、同回路記述の検証を簡便に実行することができる。
【０００８】
また、請求項２に記載の回路記述の抽象化装置は、請求項１に記載の回路記述の抽象化装置において、前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを要旨とする。
【０００９】
上記構成によれば、回路記述内に非線形の計算処理を実行する計算処理ユニットが含まれることで、同回路記述が示す論理モデルの正しさを数学的に証明することができず、形式的手法を用いた検証を適用することができない場合であっても、当該計算処理ユニットを回路記述内から適宜除外することで、同回路記述の検証を簡便に実行することができる。
【００１０】
また、請求項３に記載の回路記述の抽象化装置は、請求項１に記載の回路記述の抽象化装置において、前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを要旨とする。
【００１１】
上記構成によれば、回路記述内に過去の出力データを入力データとして再帰的に利用する計算処理ユニットが含まれることで、同回路記述が示す論理モデルの検証を短時間で実行することができず、形式的手法を用いた検証を好適に適用することができない場合であっても、当該計算処理ユニットを回路記述内から適宜除外することで、同回路記述の検証を簡便に実行することができる。
【００１２】
また、請求項４に記載の回路記述の抽象化装置は、請求項１〜請求項３のうち何れか一項に記載の回路記述の抽象化装置において、前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータを前記検証可能計算処理ユニットの入力データとして入力した場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。
【００１３】
上記構成によれば、検証可能計算処理ユニットは、検証不能計算処理ユニットの出力データに相当するデータを出力データとして出力するため、回路記述の仕様に影響を及ぼすことはなく、同回路記述の検証を正確且つ簡便に実行することができる。また、検証可能計算処理ユニットは、入力データに対して計算処理を施すことがないため、同ユニット内における処理負荷を低減することができる。
【００１４】
また、請求項５に記載の回路記述の抽象化装置は、請求項１〜請求項３のうち何れか一項に記載の回路記述の抽象化装置において、前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。
【００１５】
上記構成によれば、検証可能計算処理ユニットは、検証不能計算処理ユニットの出力データに相当するデータを出力データとして出力するため、回路記述の仕様に影響を及ぼすことはなく、同回路記述の検証を正確且つ簡便に実行することができる。また、ユーザは、検証可能計算処理ユニット内のデータ記憶部に記憶されているデータの中から出力データとして出力するものを入力データの入力により適宜選択できるため、検証不能計算処理ユニットに含まれる計算処理をユーザが実際に手作業で行う場合と比較して、同データの決定に要する手間を軽減することができる。
【００１６】
また、請求項６に記載の回路記述の検証装置は、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの検証の処理手順を制御する制御手段とを備えた回路記述の検証装置であって、前記制御手段は、予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶手段と、前記論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定手段と、該ユニット判定手段の判定結果が肯定判定である場合に、前記ユニット記憶手段に記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力手段と、前記検証不能計算処理ユニットを前記ユニット出力手段が出力した前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換手段と該ユニット置換手段により計算処理ユニットが置換された前記論理モデルを検証対象にした検証作業を実行する検証手段とを備えたことを要旨とする。上記構成によれば、請求項１に記載の発明と同様の効果が得られる。
【００１７】
また、請求項７に記載の回路記述の検証装置は、請求項６に記載の回路記述の検証装置において、前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項２に記載の発明と同様の効果が得られる。
【００１８】
また、請求項８に記載の回路記述の検証装置は、請求項６に記載の回路記述の検証装置において、前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項３に記載の発明と同様の効果が得られる。
【００１９】
また、請求項９に記載の回路記述の検証装置は、請求項６〜請求項８のうち何れか一項に記載の回路記述の検証装置において、前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータを前記検証可能計算処理ユニットの入力データとして入力した場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。上記構成によれば、請求項４に記載の発明と同様の効果が得られる。
【００２０】
また、請求項１０に記載の回路記述の検証装置は、請求項６〜請求項８のうち何れか一項に記載の回路記述の検証装置において、前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。上記構成によれば、請求項５に記載の発明と同様の効果が得られる。
【００２１】
また、請求項１１に記載の回路記述の抽象化プログラムは、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの抽象化の処理手順を制御する制御手段とを備えた回路記述の抽象化装置を稼動させるために用いられる回路記述の抽象化プログラムであって、前記制御手段を、予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶手段、前記論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定手段、該ユニット判定手段の判定結果が肯定判定である場合に、前記ユニット記憶手段に記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力手段、及び、前記検証不能計算処理ユニットを前記ユニット出力手段が出力した前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換手段として機能させることを要旨とする。上記構成によれば、請求項１に記載の発明と同様の効果が得られる。
【００２２】
また、請求項１２に記載の回路記述の抽象化プログラムは、請求項１１に記載の回路記述の抽象化プログラムにおいて、前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項２に記載の発明と同様の効果が得られる。
【００２３】
また、請求項１３に記載の回路記述の抽象化プログラムは、請求項１１に記載の回路記述の抽象化プログラムにおいて、前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項３に記載の発明と同様の効果が得られる。
【００２４】
また、請求項１４に記載の回路記述の抽象化プログラムは、請求項１１〜請求項１３のうち何れか一項に記載の回路記述の抽象化プログラムにおいて、前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータが前記検証可能計算処理ユニットの入力データとして入力された場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力させる計算処理ユニットであることを要旨とする。上記構成によれば、請求項４に記載の発明と同様の効果が得られる。
【００２５】
また、請求項１５に記載の回路記述の抽象化プログラムは、請求項１１〜請求項１３のうち何れか一項に記載の回路記述の抽象化プログラムにおいて、前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。上記構成によれば、請求項５に記載の発明と同様の効果が得られる。
【００２６】
また、請求項１６に記載の回路記述の検証プログラムは、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの検証の処理手順を制御する制御手段とを備えた回路記述の検証装置を稼動させるために用いられる回路記述の検証プログラムであって、前記制御手段を、予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶手段、前記論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定手段、該ユニット判定手段の判定結果が肯定判定である場合に、前記ユニット記憶手段に記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力手段、前記検証不能計算処理ユニットを前記ユニット出力手段が出力した前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換手段、及び、該ユニット置換手段により計算処理ユニットが置換された前記論理モデルを検証対象にした検証作業を実行する検証手段として機能させることを要旨とする。上記構成によれば、請求項６に記載の発明と同様の効果が得られる。
【００２７】
また、請求項１７に記載の回路記述の検証プログラムは、請求項１６に記載の回路記述の検証プログラムにおいて、前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項７に記載の発明と同様の効果が得られる。
【００２８】
また、請求項１８に記載の回路記述の検証プログラムは、請求項１６に記載の回路記述の検証プログラムにおいて、前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項８に記載の発明と同様の効果が得られる。
【００２９】
また、請求項１９に記載の回路記述の検証プログラムは、請求項１６〜請求項１８のうち何れか一項に記載の回路記述の検証プログラムにおいて、前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータが前記検証可能計算処理ユニットの入力データとして入力された場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。上記構成によれば、請求項９に記載の発明と同様の効果が得られる。
【００３０】
また、請求項２０に記載の回路記述の検証プログラムは、請求項１６〜請求項１８のうち何れか一項に記載の回路記述の検証プログラムにおいて、前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。上記構成によれば、請求項１０に記載の発明と同様の効果が得られる。
【００３１】
また、請求項２１に記載の回路記述の抽象化方法は、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の抽象化方法であって、予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶段階と、前記回路記述が示す論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定段階と、該ユニット判定段階の判定結果が肯定判定である場合に、前記ユニット記憶段階にて記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力段階と、前記検証不能計算処理ユニットを前記ユニット出力段階で出力された前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された前記検証可能計算処理ユニットに置換するユニット置換段階とを備えたことを要旨とする。上記構成によれば、請求項１に記載の発明と同様の効果が得られる。
【００３２】
また、請求項２２に記載の回路記述の抽象化方法は、請求項２１に記載の回路記述の抽象化方法において、前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項２に記載の発明と同様の効果が得られる。
【００３３】
また、請求項２３に記載の回路記述の抽象化方法は、請求項２１に記載の回路記述の抽象化方法において、前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項３の発明と同様の効果が得られる。
【００３４】
また、請求項２４に記載の回路記述の抽象化方法は、請求項２１〜請求項２３のうち何れか一項に記載の回路記述の抽象化方法において、前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータが前記検証可能計算処理ユニットの入力データとして入力された場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。上記構成によれば、請求項４に記載の発明と同様の効果が得られる。
【００３５】
また、請求項２５に記載の回路記述の抽象化方法は、請求項２１〜請求項２３のうち何れか一項に記載の回路記述の抽象化方法において、前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。上記構成によれば、請求項５に記載の発明と同様の効果が得られる。
【００３６】
また、請求項２６に記載の回路記述の検証方法は、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の検証方法であって、予め設定した閾値時間内に形式的手法による検証を実行可能な検証可能計算処理ユニットを少なくとも一つ記憶するユニット記憶段階と、前記回路記述が示す論理モデル内に含まれる少なくとも一つの計算処理ユニットに対して、該計算処理ユニットが前記閾値時間内に形式的手法による検証を実行不能な検証不能計算処理ユニットであるか否かを判定するユニット判定段階と、該ユニット判定段階の判定結果が肯定判定である場合に、前記ユニット記憶段階にて記憶された前記検証可能計算処理ユニットを選択可能に出力するユニット出力段階と、前記検証不能計算処理ユニットを前記ユニット出力段階で出力された前記検証可能計算処理ユニットのうちから前記検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットに置換するユニット置換段階と、該ユニット置換段階にて計算処理ユニットが置換された前記論理モデルを検証対象にした検証作業を実行する検証段階とを備えたことを要旨とする。上記構成によれば、請求項６に記載の発明と同様の効果が得られる。
【００３７】
また、請求項２７に記載の回路記述の検証方法は、請求項２６に記載の回路記述の検証方法において、前記検証不能計算処理ユニットは、非線形の計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項７に記載の発明と同様の効果が得られる。
【００３８】
また、請求項２８に記載の回路記述の検証方法は、請求項２６に記載の回路記述の検証方法において、前記検証不能計算処理ユニットは、前記回路記述に含まれる計算処理ユニットの出力データを記憶する出力データ記憶部を有しており、該出力データ記憶部に記憶された出力データを読み出し、且つ該読み出した出力データを再帰的に入力データとして利用する計算処理を実行する計算処理ユニットであることを要旨とする。上記構成によれば、請求項８に記載の発明と同様の効果が得られる。
【００３９】
また、請求項２９に記載の回路記述の検証方法は、請求項２６〜請求項２８のうち何れか一項に記載の回路記述の検証方法において、前記検証可能計算処理ユニットは、前記検証不能計算処理ユニットの出力データに相当するデータが前記検証可能計算処理ユニットの入力データとして入力された場合に、該入力データに対して計算処理を施すことなく前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。上記構成によれば、請求項９に記載の発明と同様の効果が得られる。
【００４０】
また、請求項３０に記載の回路記述の検証方法は、請求項２６〜請求項２８のうち何れか一項に記載の回路記述の検証方法において、前記検証可能計算処理ユニットは、該検証可能計算処理ユニットに入力される入力データと対応付けて前記検証不能計算処理ユニットの出力データに相当するデータを少なくとも一つ記憶するデータ記憶部を有しており、前記入力データが入力された場合に、該入力データに対応するデータを前記データ記憶部から読み出し、該読み出したデータを前記検証可能計算処理ユニットの出力データとして出力する計算処理ユニットであることを要旨とする。上記構成によれば、請求項１０に記載の発明と同様の効果が得られる。
【発明を実施するための最良の形態】
【００４１】
（第１の実施形態）
以下、本発明を具体化した第１の実施形態を図１〜図３に従って説明する。
図１に示すように、本実施形態におけるコンピュータシステム１０は、制御装置１１、入力装置１２、出力装置１３、読み込み装置１４、及びディスク装置１５を備えている。そして、コンピュータシステム１０は、これらの各装置１１〜１５がバス１６を介して相互に情報を伝達可能に接続されることにより、回路記述の抽象化装置及び検証装置として各種の情報処理を行い得るように構成されている。なお、読み込み装置１４には、ＣＤ（Ｃｏｍｐａｃｔ  Ｄｉｓｃ）などの記録媒体１７が挿脱可能とされている。そして、本実施形態では、この読み込み装置１４に対してプログラム言語を用いて記述された検証対象となるプログラムデータを記録した記録媒体１７及びこのプログラム言語を用いて記述されたプログラムデータの記述内容を形式的仕様記述言語による回路記述に変換する際に使用するモデリング変換ソフト（Ｓｉｍｕｌｉｎｋ、Ｓｃａｄｅ等）を記録した記録媒体１７が選択的に挿脱されるようになっている。
【００４２】
制御装置１１は、コンピュータシステム１０の稼動状態を制御するための制御手段として機能するものであり、その具体的構成については後述する。入力装置１２は、キーボードやマウス等を備えてなり、各種情報を手入力する場合に使用される。出力装置１３は、入力装置１２を介して入力された各種情報の内容を出力して表示可能なＣＲＴディスプレイ等を備えている。読み込み装置１４は、ＣＤ等の記録媒体１７が挿入された場合に該記録媒体１７に記録されているプログラムデータ等の各種データを読み込む。そして、ディスク装置１５は、読み込み装置１４により読み込まれた各種データを保存可能な記憶手段として機能する。
【００４３】
図１に示すように、制御装置１１は、外部装置との間の情報のやり取りを仲介するインターフェース（図示略）、中央処理装置としてのＣＰＵ１８、所定の情報を読み出し可能に記憶するＲＯＭ１９、及び各種の情報を書き込み／読み出し可能に記憶するＲＡＭ２０を備えたデジタルコンピュータとして構成されている。そして、こうした制御装置１１がデジタルコンピュータとして機能するように、ＣＰＵ１８は、インターフェースを介して各種の情報が入力された場合に、回路記述の抽象化及び抽象化された回路記述の検証のために必要とされる各種の論理演算を行うと共に、その論理演算において使用される各種情報の読み出し及び書き込みを行う。また、ＲＯＭ１９には、回路記述の抽象化処理、及び、抽象化された回路記述の検証処理に際して、ＣＰＵ１８がコンピュータシステム１０全体の稼動状態を制御するために用いる抽象化プログラム２１及び検証プログラム２２が記憶されている。また、ＲＡＭ２０には、コンピュータシステム１０の稼動中にＣＰＵ１８による論理演算において使用されると共に書き換えられる各種の情報内容が適宜記憶されるようになっている。
【００４４】
モデリング変換ソフト（例えば、Ｓｉｍｕｌｉｎｋ）を記録した記録媒体１７が読み込み装置１４に挿入された場合、ＣＰＵ１８は、その記録媒体１７に記録されたモデリング変換ソフトのデータ内容を読み込み装置１４により読み込ませ、その読み込みデータ内容をディスク装置１５にモデリングツール２３として記憶させる。また、プログラム言語を用いて記述された検証対象となるプログラムデータを記録した記録媒体１７が読み込み装置１４に挿入された場合、ＣＰＵ１８は、その記録媒体１７に記録されたプログラムデータをＲＡＭ２０に一旦記憶させる。そして次に、ディスク装置１５に記憶させたモデリングツール２３を起動させることにより、ＲＡＭ２０に一旦記憶させたプログラムデータを形式的仕様記述言語による回路記述の仕様データ２４に変換し、その変換した回路記述の仕様データ２４をディスク装置１５に記憶させる。
【００４５】
ＣＰＵ１８は、ＲＯＭ１９に記憶した抽象化プログラム２１を起動した場合に、ディスク装置１５に記憶させた回路記述の仕様データ２４が表す論理モデルに含まれる複数の計算処理ユニットを出力装置１３のディスプレイに表示させる。そして、ＣＰＵ１８は、その出力装置１３のディスプレイに表示された各計算処理ユニットに対して、検証プログラム２２による検証処理を予め設定した閾値時間内に実行可能な検証可能計算処理ユニットであるか、或いは、同検証処理を予め設定した閾値時間内に実行不能な検証不能計算処理ユニットであるかをそれぞれ判定する。この点で、ＣＰＵ１８は、論理モデル内の各計算処理ユニットについて、検証プログラム２２の検証対象として好適であるか否かを判定するユニット判定手段としてのユニット判定部２５を備えているといえる。
【００４６】
また、ＣＰＵ１８は、検証可能計算処理ユニットの一覧のデータ内容を記録した記録媒体１７が読み込み装置１４に挿入された場合に、その記録媒体１７に記録されたデータ内容をＲＡＭ２０に一旦記憶させる。この点で、制御装置１１が備えるＲＡＭ２０はユニット記憶手段としてのユニット記憶部２６を備えているといえる。そして、こうした読み込み装置１４を用いた検証可能計算処理ユニットの一覧の記憶段階がユニット記憶段階に相当する。
【００４７】
また、ＣＰＵ１８は、論理モデル内の各計算処理ユニットについて、ユニット判定部２５により検証不能計算処理ユニットであると判定された場合には、ＲＡＭ２０のユニット記憶部２６に一時記憶された検証可能計算処理ユニットの一覧を、入力装置１２からの入力操作に基づき選択可能な態様で出力装置１３のディスプレイに出力して表示する。この点で、ＣＰＵ１８は、ユニット出力手段としてのユニット出力部２７を備えているといえる、
また、ＣＰＵ１８は、ユニット出力部２７により出力結果として出力される検証可能計算処理ユニットの一覧のうち、入力装置１２の入力操作に基づき検証不能計算処理ユニットに対応するものとして選択された検証可能計算処理ユニットをＲＡＭ２０から読み出す。そして、論理モデル内にて、ユニット判定部２５にて検証不能計算処理ユニットとして判定された計算処理ユニットを、ＲＡＭ２０から読み出した検証可能計算処理ユニットに置換し、置換した検証可能計算処理ユニットを含む論理モデルを表す回路記述の仕様データ２４をディスク装置１５に既に記憶されている仕様データ２４に上書きして保存する。この点で、ＣＰＵ１８は、ユニット置換手段としてのユニット置換部２８を備えているといえる。
【００４８】
また、ＣＰＵ１８は、ＲＯＭ１９に記憶した検証プログラム２２を起動した場合に、ユニット置換部２８にて上書き保存された回路記述の仕様データ２４をディスク装置１５から読み出し、読み出した仕様データ２４で表される論理モデルに対して検証作業を実行する。この点で、ＣＰＵ１８は、検証手段としての検証部２９を備えているといえる。
【００４９】
次に、検証不能計算処理ユニットとしての非線形計算処理ユニット３０について、図２（ａ）に基づき説明する。
図２（ａ）に示すように、本実施形態の非線形計算処理ユニット３０は、第１のプロダクトブロック３１、第２のプロダクトブロック３２、第３のプロダクトブロック３３、第１のコンスタントブロック３４、及び第２のコンスタントブロック３５により構成されている。第１のプロダクトブロック３１は、入力装置１２を介して設定された２つの数値データＩｎ１，Ｉｎ２がインポートブロック３６，３７を通じてそれぞれ入力された場合に、それらの数値データＩｎ１，Ｉｎ２に対して乗算又は除算を実行するようになっている。第２のプロダクトブロック３２は、第１のプロダクトブロック３１の出力データに対して第１のコンスタントブロック３４から新たに入力される数値データ（本実施形態では「６０」の数値）の乗算を実行するようになっている。第３のプロダクトブロック３３は、第２のプロダクトブロック３２の出力データに対して第２のコンスタントブロック３５から新たに入力される数値データ（本実施形態では「２＊ｐｉ」、Ｐｉ：ユーザが予め設定する登録定数）の乗算を実行するようになっている。すなわち、非線形計算処理ユニット３０では、２つの変数（即ち、Ｉｎ１，Ｉｎ２）を入力データとして、これらのデータに対して乗算又は除算を実行することで１つの出力データを出力するため、出力データは、入力データに対して非線形の２変数関数で規定される相関関係を有することとなる。
【００５０】
続いて、検証可能計算処理ユニットとしての線形計算処理ユニット３８について、図２（ｂ）に基づき説明する。
図２（ｂ）に示すように、本実施形態の線形計算処理ユニット３８は、入力装置１２を介して設定された１つの数値データＩｎ３がインポートブロック３９を通じて入力された場合に、その数値データＩｎ３に対して演算処理を実行することなく出力データとして直接出力する非処理ブロック４０により構成されている。すなわち、線形計算処理ユニット３８では、常に、入力データに対して同値となる数値データを出力データとして出力するため、出力データは、入力データに対して線形の１次関数で規定される相関関係を有することとなる。
【００５１】
次に、本実施形態のＣＰＵ１８が抽象化プログラム２１の起動に伴い実行するユニット置換処理ルーチンについて図３に基づき説明する。
まず、ＣＰＵ１８は、回路記述の仕様データ２４で表される論理モデル内に含まれる複数の計算処理ユニットのうち、１つの計算処理ユニットを選択する（ステップＳ１１）。
【００５２】
続いて、ユニット判定段階として、ＣＰＵ１８は、ステップＳ１１にて選択した計算処理ユニットが非線形の計算処理を実行する非線形計算処理ユニット３０であるか否かを判定する（ステップＳ１２）。そして、ステップＳ１２の判定結果が肯定判定である場合、ユニット出力段階として、ＣＰＵ１８は、その計算処理ユニットが形式的手法を用いた検証を適用できない非線形計算処理ユニット３０（検証不能計算処理ユニット）であると判断し、線形計算処理ユニット３８（検証可能計算処理ユニット）の一覧をＲＡＭ２０から読み出し、読み出した線形計算処理ユニット３８の一覧を出力装置１３に出力して表示する。（ステップＳ１３）。一方、ステップＳ１２の判定結果が否定判定である場合、ＣＰＵ１８は、その計算処理ユニットが形式的手法を用いた検証を好適に適用できる計算処理ユニットであると判断し、その処理をステップＳ１５に移行する。
【００５３】
そして次に、ステップＳ１３にて出力された線形計算処理ユニット３８の一覧のうち、１つの線形計算処理ユニット３８が入力装置１２の入力操作を通じて選択された場合、ユニット置換段階として、ＣＰＵ１８は、論理モデル内にて、選択された線形計算処理ユニット３８とステップＳ１１にて選択した計算処理ユニット（すなわち、非線形計算処理ユニット３０）とを置換する（ステップＳ１４）。そして、置換した線形計算処理ユニット３８を含んで構成される論理モデルを表す回路記述の仕様データ２４をディスク装置１５に既に記憶されている仕様データ２４に上書きして保存する。
【００５４】
続いて、ＣＰＵ１８は、回路記述の仕様データ２４で表される論理モデル内の全ての計算処理ユニットについて、非線形の計算処理に関する検証が完了したか否かを判断する（ステップＳ１５）。そして、ステップＳ１５の判定結果が否定判定である場合、ＣＰＵ１８は、本処理をステップＳ１１に戻して、再度、論理モデル内から計算処理ユニットを新たに選択する。そして、以後、ステップＳ１１〜ステップＳ１４までの処理を繰り返す。一方、ステップＳ１５の判定結果が肯定判定である場合、ＣＰＵ１８は、抽象化プログラム２１のユニット置換処理ルーチンを終了する。
【００５５】
その後、ディスク装置１５に記憶されている回路記述の仕様データ２４に基づき検証対象とされるプログラム内容を検証する場合、ＣＰＵ１８は、検証段階として、ＲＯＭ１９に記憶している検証プログラム２２を起動して、ディスク装置１５に記憶されている回路記述の仕様データ２４を読み出す。そして、ＣＰＵ１８は、その仕様データ２４により表される論理モデルを検証対象にして、形式的手法を用いた各種デバッグ用の検証を実行する。
【００５６】
さて、回路記述の仕様データ２４で表される論理モデル内に非線形の計算処理を実行する計算処理ユニットが含まれる場合には、同モデルの正しさを数学的に証明することができず、形式的手法を用いた検証を適用することができないという問題があるところ、本実施形態のコンピュータシステム１０によれば、論理モデル内に非線形計算処理ユニット３０が含まれていることを検出した場合には、該非線形計算処理ユニット３０を線形計算処理ユニット３８に半自動的に置換する構成となっている。そのため、形式的手法を用いた検証に適さない非線形計算処理ユニット３０を含む論理モデルを、形式的手法を用いた検証に適した形式的仕様に簡便に変換することができる。
【００５７】
本実施形態によれば、以下の効果を得ることができる。
（１）上記実施形態では、回路記述の仕様データ２４で表される論理モデル内に非線形の計算処理を実行する非線形計算処理ユニット３０を含むことで、同モデルの正しさを数学的に証明することができず、形式的手法を用いた検証を適用できない場合であっても、非線形計算処理ユニット３０を線形計算処理ユニット３８に半自動的に置換して抽象化することで、同モデルの検証を簡便に実行することができる。
【００５８】
（２）上記実施形態では、線形計算処理ユニット３８には、非線形計算処理ユニット３０の出力データに相当するデータがインポートブロック３９を介して入力されるため、回路記述の仕様データ２４で表される論理モデルの形式的仕様に影響を及ぼすことはなく、同モデルの検証を正確且つ簡便に実行することができる。また、線形計算処理ユニット３８は、入力データに対して計算処理を施すことがないため、同ユニット内における処理負荷を低減することができる。
【００５９】
（第２の実施形態）
次に、本発明の第２の実施形態を図４及び図５に従って説明する。なお、この第２の実施形態は第１の実施形態との対比において次の点で構成が相違している。すなわち、本実施形態では、検証不能計算処理ユニットが、過去のデータを入力データとして再帰的に利用する再帰計算処理ユニットである点が第１の実施形態と異なっている。したがって、以下の説明においては、第１の実施形態と同一又は相当する部材構成については同一符号を付して重複説明を省略するものとする。
【００６０】
まず、検証不能計算処理ユニットとしての再帰計算処理ユニット４１について、図４（ａ）に基づき説明する。
図４（ａ）に示すように、本実施形態の再帰計算処理ユニット４１は、スイッチブロック４２、メモリブロック４３、サムブロック４４、第１のコンスタントブロック４５、及び第２のコンスタントブロック４６により構成されている。スイッチブロック４２は、入力装置１２を介して設定された１つの数値データＩｎ１がインポートブロック４７を通じて制御入力として入力された場合に、その数値データＩｎ１に応じてデータ入力として入力された２つの数値データのうち何れを出力データとして通過させるかを切り替えるようになっている。また、メモリブロック４３は、スイッチブロック４２から出力されたデータを記憶し、記憶したデータを後の時間ステップで出力データとして出力するようになっている。すなわち、メモリブロック４３は、再帰計算処理ユニット４１の出力データとしてスイッチブロック４２から出力されたデータを記憶する出力データ記憶部として機能する。また、サムブロック４４は、メモリブロック４３から出力されたデータに対して第１のコンスタントブロック４５から新たに入力された数値データ（本実施形態では「１」）の加算を実行し、そのデータをデータ入力としてスイッチブロック４２に入力するようになっている。なお、スイッチブロック４２には、データ入力として、第２のコンスタントブロック４６から数値データ（本実施形態では「０」の数値）が入力されるようになっている。
【００６１】
次に、検証可能計算処理ユニットとしての非再帰計算処理ユニット４８について、図４（ｂ）に基づき説明する。
図４（ｂ）に示すように、本実施形態の非再帰計算処理ユニット４８は、非処理ブロック４９、サムブロック５０、スイッチブロック５１、第１のコンスタントブロック５２、及び第２のコンスタントブロック５３により構成されている。非処理ブロック４９は、１つの数値データＩｎ２がインポートブロック５４を通じて入力された場合に、その数値データＩｎ２に対して演算処理を実行することなく、サムブロック５０に対して出力データとして直接出力するようになっている。サムブロック５０は、非処理ブロック４９からの出力データに対して第１のコンスタントブロック５２から新たに入力された数値データ（本実施形態では「１」の数値）の加算を実行し、そのデータをデータ入力としてスイッチブロック５１に入力するようになっている。スイッチブロック５１は、１つの数値データＩｎ１がインポートブロック５５を通じて制御入力として入力された場合に、その数値データＩｎ１に応じてデータ入力として入力された２つの数値データのうち何れを出力データとして通過させるかを切り替えるようになっている。なお、スイッチブロック５１には、データ入力として、第２のコンスタントブロック５３から数値データ（本実施形態では「０」の数値）が入力されるようになっている。
【００６２】
次に、本実施形態のＣＰＵ１８が抽象化プログラム２１の起動に伴い実行するユニット置換処理ルーチンについて図５に基づき説明する。
まず、ＣＰＵ１８は、回路記述の仕様データ２４で表される論理モデル内に含まれる複数の計算処理ユニットのうち、１つの計算処理ユニットを選択する（ステップＳ２１）。
【００６３】
そして次に、ユニット判定段階として、ＣＰＵ１８は、ステップＳ１０にて選択した計算処理ユニットが、過去の出力データを入力データとして利用する計算処理ブロック（本実施形態ではメモリブロック４３）を含んで構成される再帰計算処理ユニット４１であるか否かを判定する（ステップＳ２２）。そして、ステップＳ２２の判定結果が肯定判定である場合、ＣＰＵ１８は、その計算処理ユニットが形式的手法を用いた検証を実行する場合に過度の処理負荷を要し、同検証に好適に適用できない再帰計算処理ユニット４１（検証不能計算処理ユニット）であると判断し、非再帰計算処理ユニット４８（検証可能計算処理ユニット）の一覧をＲＡＭ２０から読み出し、読み出した非再帰計算処理ユニット４８の一覧を出力装置１３に出力して表示する（ステップＳ２３）。一方、ステップＳ２２の判定結果が否定判定である場合、ＣＰＵ１８は、その計算処理ユニットが形式的手法を用いた検証を好適に適用できる計算処理ユニットであると判断し、その処理をステップＳ２５に移行する。
【００６４】
続いて、ステップＳ１２にて出力された非再帰計算処理ユニット４８の一覧のうち、１つの非再帰計算処理ユニット４８が入力装置１２の入力操作を通じて選択された場合、ユニット置換段階として、ＣＰＵ１８は、論理モデル内にて、選択された非再帰計算処理ユニット４８とステップＳ２１にて選択した計算処理ユニット（すなわち、再帰計算処理ユニット４１）とを置換する（ステップＳ２４）。そして、置換した非再帰計算処理ユニット４８を含んで構成される論理モデルを表す回路記述の仕様データ２４をディスク装置１５に既に記憶されている仕様データ２４に上書きして保存する。
【００６５】
そして次に、ＣＰＵ１８は、回路記述の仕様データ２４で表される論理モデル内の全ての計算処理ユニットについて、再帰計算処理ユニット４１に関する検証が完了したか否かを判断する（ステップＳ２５）。そして、ステップＳ２５の判定結果が否定判定である場合、ＣＰＵ１８は、その処理をステップＳ２１に戻して、再度、論理モデル内から計算処理ユニットを新たに選択する。そして、以後、ステップＳ２１〜ステップ２４までの処理を繰り返す。一方、ステップＳ２５の判定結果が肯定判定である場合、ＣＰＵ１８は、抽象化プログラム２１の起動に基づいたユニット置換処理ルーチンを終了する。
【００６６】
その後、ディスク装置１５に記憶されている回路記述の仕様データ２４に基づき検証対象とされるプログラム内容を検証する場合、ＣＰＵ１８は、検証段階として、ＲＯＭ１９に記憶している検証プログラム２２を起動して、ディスク装置１５に記憶されている回路記述の仕様データ２４を読み出す。そして、ＣＰＵ１８は、その仕様データ２４により表される論理モデルを検証対象にして、形式的手法を用いた各種デバッグ用の検証を実行する。
【００６７】
さて、回路記述の仕様データ２４で表される論理モデル内に過去の出力データを入力データとして再帰的に利用する計算処理を実行する再帰計算処理ユニット４１が含まれる場合には、過去の出力データを読み出す際に、同計算処理ユニット内の計算処理を繰り返し実行することで過大な処理負荷を生じるため、形式的手法を用いた検証に膨大な時間を要するという問題があるところ、本実施形態のコンピュータシステム１０によれば、論理モデル内に再帰計算処理ユニット４１が含まれていることを検出した場合には、該再帰計算処理ユニット４１を非再帰計算処理ユニット４８に半自動的に置換する構成となっている。そのため、形式的手法を用いた検証に適さない再帰計算処理ユニット４１を含む論理モデルを、形式的手法を用いた検証に適した形式的仕様に簡便に変換することができる。
【００６８】
したがって、本実施形態では、以下に示す効果を得ることができる。
（３）上記実施形態では、回路記述の仕様データ２４で表される論理モデル内に、過去の出力データを入力データとして再帰的に利用する計算処理を実行する再帰計算処理ユニット４１を含むことで、過去の出力データを読み出す際に、同計算処理ユニット内の計算処理を繰り返し実行することで過大な処理負荷を生じ、形式的手法を用いた検証を好適に適用できない場合であっても、再帰計算処理ユニット４１を非再帰計算処理ユニット４８に半自動的に置換して抽象化することで、同モデルの検証を簡便に実行することができる。
【００６９】
（４）上記実施形態では、非再帰計算処理ユニット４８では、再帰計算処理ユニット４１におけるメモリブロック４３の出力データに相当する数値データがインポートブロック５４を介して入力されるため、回路記述の仕様データ２４で表される論理モデルの形式的仕様に影響を及ぼすことはなく、同モデルの検証を正確且つ簡便に実行することができる。
【００７０】
なお、上記実施形態は以下のような別の実施形態に変更してもよい。
・上記第１の実施形態において、図６に示すように、検証可能計算処理ユニットとしての線形計算処理ユニット５６は、制御入力として入力された数値データに応じて、データ入力として入力された複数の数値データのうち何れを出力データとして通過させるかを切り替えるスイッチブロック５７を含んで構成してもよい。この場合、スイッチブロック５７にデータ入力として入力される数値データは、図２（ａ）に示す非線形計算処理ユニット３０内にて、インポートブロック３６，３７を通じて２つの数値データＩｎ１，Ｉｎ２を第１のプロダクトブロック３１に入力した場合に出力データとして得られる数値データをユーザが予め想定し（本実施形態では「０」「１００」「２００」の各数値）、その想定した数値データに対して第２のプロダクトブロック３２及び第３のプロダクトブロック３３で施される演算処理を実行することで算出される値として決定される。なお、これらの値は、線形計算処理ユニット５６内にて、非線形計算処理ユニット３０の出力データに相当するデータとして、データ記憶部としてのコンスタントブロック５８，５９，６０にそれぞれ記憶されている。そして、スイッチブロック５７は、入力装置１２を介して設定された数値データＩｎ１がインポートブロック３９を通じて制御入力として入力された場合に、その数値データＩｎ１に応じて、各コンスタントブロック５８〜６０からデータ入力として入力された数値データのうち何れを出力データとして通過させるかを切り替えるようになっている。すなわち、線形計算処理ユニット５６は、スイッチブロック５７に制御入力として入力されるデータと、非線形計算処理ユニット３０の出力データに相当するデータとを対応づけて記憶しており、入力データが入力された場合に、入力データに対応するデータを読み出して、読み出したデータを線形計算処理ユニット５６の出力データとして出力するようになっている。
【００７１】
この構成によれば、線形計算処理ユニット５６は、非線形計算処理ユニット３０の出力データに相当するデータを出力データとして出力するため、回路記述の仕様に影響を及ぼすことはなく、同回路記述の検証を正確且つ簡便に実行することができる。また、ユーザは、線形計算処理ユニット５６内の各コンスタントブロック５８〜６０に記憶されているデータの中から出力データとして出力するものを適宜選択するため、非線形計算処理ユニット３０に含まれる計算処理をユーザが実際に行うことで同データを算出する場合と比較して、同データの決定に要する手間を軽減することができる。なお、線形計算処理ユニット５６を構成するデータ記憶部としてのコンスタントブロックの数は３つに限定されず、少なくとも１つを含んでいればよい。
【００７２】
・上記第２の実施形態において、図７に示すように、検証可能計算処理ユニットとしての非再帰計算処理ユニット６２は、制御入力として入力された数値データに応じて、データ入力として入力された複数の数値データのうち何れを出力データとして通過させるかを切り替えるスイッチブロック６３を含んで構成してもよい。この場合、スイッチブロック６３にデータ入力として入力される数値データは、図４（ａ）に示す再帰計算処理ユニット４１内にて、メモリブロック４３から読み出されてサムブロック４４の入力データとして入力される数値データをユーザが予め想定することで決定される（本実施形態では「０」「１」「１０」「２５４」「２５５」）。なお、これらの数値データは、データ記憶部としてのコンスタントブロック６４，６５，６６，６７，６８にそれぞれ記憶されている。そして、スイッチブロック６３は、入力装置１２を介して設定された数値データＩｎ１がインポートブロックを通じて制御入力として入力された場合に、その数値データＩｎ１に応じて、各コンスタントブロック６４〜６８からデータ入力として入力された数値データのうち何れを出力データとして通過させるかを切り替えるようになっている。すなわち、非再帰計算処理ユニット６２は、スイッチブロック６３に制御入力として入力されるデータと、再帰計算処理ユニット４１の出力データに相当するデータとを対応づけて記憶しており、入力データが入力された場合に、入力データに対応するデータを読み出して、読み出したデータを非再帰計算処理ユニット６２の出力データとして出力するようになっている。
【００７３】
この構成によれば、非再帰計算処理ユニット６２は、再帰計算処理ユニット４１の出力データに相当するデータを出力データとして出力するため、回路記述の仕様に影響を及ぼすことはなく、同回路記述の検証を正確且つ簡便に実行することができる。また、ユーザは、非再帰計算処理ユニット６２内の各コンスタントブロック６４〜６８に記憶されているデータの中から出力データとして出力するものを適宜選択するため、メモリブロックに記憶されているデータ群を抽出して、抽出したデータ群から適切なデータを選択する場合と比較して、同データの決定に要する手間を軽減することができる。なお、非再帰計算処理ユニット６２を構成するデータ記憶部としてのコンスタントブロックの数は５つに限定されず、少なくとも１つを含んでいればよい。
【００７４】
・上記第２の実施形態において、ＣＰＵ１８のユニット判定部２５は、論理モデル内に含まれる複数の計算処理ユニットのうち、一部の計算処理ユニットについて、過去の出力データを入力データとして利用する計算処理ブロックを含んで構成される再帰計算処理ユニット４１であるか否かを判定する構成としてもよい。
【００７５】
・上記各実施形態において、ＣＰＵ１８は、記録媒体１７に記録された複数の検証可能計算処理ユニットのうち、一部の検証可能計算処理ユニットのデータ内容をＲＡＭ２０のユニット記憶部２６に一時記憶させるようにしてもよい。
【００７６】
・上記各実施形態において、ＣＰＵ１８は、入力装置１２の入力操作を通じて入力された複数の検証可能計算処理ユニットのデータ内容をＲＡＭ２０のユニット記憶部２６に一時記憶させるようにしてもよい。
【００７７】
・上記各実施形態において、抽象化プログラム２１に検証可能計算処理ユニットの一覧のデータ内容を組み込み、ＣＰＵ１８は、抽象化プログラム２１から複数の検証可能計算処理ユニットのデータ内容を読み込んでＲＡＭ２０のユニット記憶部２６に一時記憶させるようにしてもよい。
【００７８】
・上記各実施形態において、ＣＰＵ１８のユニット出力部２７は、ＲＡＭ２０のユニット記憶部２６により記憶された複数の検証可能計算処理ユニットのうち、一部の検証可能計算処理ユニットを出力装置１３のディスプレイに出力して表示するようにしてもよい。
【００７９】
・上記各実施形態において、回路記述の仕様データ２４が表す論理モデルは、単一の計算処理ユニットにより構成してもよい。
・上記各実施形態において、抽象化プログラム２１による抽象化の対象となる検証不能計算処理ユニットとして、処理負荷が過大となる煩雑な数式処理を実行する計算処理ユニットを適用してもよい。
【図面の簡単な説明】
【００８０】
【図１】第１の実施形態のコンピュータシステムを示すブロック図。
【図２】（ａ）は第１の実施形態の非線形計算処理ユニットを示すブロック図、（ｂ）は第１の実施形態の線形計算処理ユニットを示すブロック図。
【図３】第１の実施形態の抽象化プログラムのユニット置換処理ルーチンを示すフローチャート。
【図４】（ａ）は第２の実施形態の再帰計算処理ユニットを示すブロック図、（ｂ）は第２の実施形態の非再帰計算処理ユニットを示すブロック図。
【図５】第２の実施形態の抽象化プログラムのユニット置換処理ルーチンを示すフローチャート。
【図６】別の実施形態の線形計算処理ユニットを示すブロック図。
【図７】別の実施形態の非再帰計算処理ユニットを示すブロック図。
【符号の説明】
【００８１】
１０…抽象化装置及び検証装置としてのコンピュータシステム、１１…制御手段としての制御装置、１５…記憶手段としての記憶装置、１８…ユニット判定手段、ユニット出力手段、ユニット置換手段、及び検証手段としてのＣＰＵ、２０…ユニット記憶手段としてのＲＡＭ、２１…抽象化プログラム、２２…検証プログラム、２４…回路記述の仕様データ、３０…検証不能計算処理ユニットとしての非線形計算処理ユニット、３８…検証可能計算処理ユニットとしての線形計算処理ユニット、４１…検証不能計算処理ユニットとしての再帰計算処理ユニット、４３…出力データ記憶部としてのメモリブロック、４８…検証可能計算処理ユニットとしての非再帰計算処理ユニット、５６…検証可能計算処理ユニットとしての線形計算処理ユニット、５８〜６０…データ記憶部としてのコンスタントブロック、６２…検証可能計算処理ユニットとしての非再帰計算処理ユニット、６４〜６８…データ記憶部としてのコンスタントブロック。
【図１】
2010079433.tif 000003
【図２】
2010079433.tif 000004
【図３】
2010079433.tif 000005
【図４】
2010079433.tif 000006
【図５】
2010079433.tif 000007
【図６】
2010079433.tif 000008
【図７】
2010079433.tif 000009