(57)【要約】【課題】高度な仕様や、ＩＰ間にまたがる仕様を記述できるプロパティ記述言語で書かれたアサーションを処理するデジタル回路検証のための装置及び方法を提供する。【解決手段】時相論理式判定装置の判定結果が真になった場合に、検証プログラム解釈部を駆動し、真になった時相論理式と対になっている検証プログラムを実行する。検証プログラム解釈部は、全ての検証プログラム間で共有する値を保持する共有記憶部を駆動しながら検証プログラムを実行する。【選択図】      図１
2008299629.tif 000002
【特許請求の範囲】
【請求項１】
検証対象とするデジタル回路のハードウェア設計記述の論理シミュレーションを行うと共に前記デジタル回路のハードウェア設計記述が時相論理式を満たしているかどうかを判定するハードウェア設計記述シミュレータと協働し、前記時相論理式、及び前記時相論理式が表現する命題が真になったときに実行すべき検証プログラムの組の集合からなるアサーションを入力として前記デジタル回路の機能を検証するデジタル回路検証装置であって、
前記ハードウェア設計記述シミュレータから前記時相論理式の判定結果を受け取り、前記判定結果に対応する検証プログラムを選択する検証プログラム選択部と、
前記集合における検証プログラムの全ての間で共有される値を記憶する共有記憶部と、
前記検証プログラム選択部により選択された検証プログラムを前記共有記憶部に記憶された値を参照しながら解釈し、前記共有記憶部への値の書込を行う検証プログラム解釈部と、
前記検証プログラム解釈部による前記検証プログラムの解釈結果を前記デジタル回路の検証結果として出力する出力部と、を具備することを特徴とするデジタル回路検証装置。
【請求項２】
前記検証プログラム内に記述されている変数の実体が、前記デジタル回路内の信号の値であるか、前記共有記憶部内の値であるかを判定する変数実体判定部と、
前記変数実体判定部により判定された変数の実体から値を読み込む変数読込部と、
前記変数実体判定部により判定された変数の実体に対して値を書き込む変数書込部とをさらに具備することを特徴とする請求項１記載のデジタル回路検証装置。
【請求項３】
前記時相論理式の判定結果を前記検証プログラム選択部に伝えるために、
ハードウェア設計記述シミュレータが外部プログラムと通信するために予め備えているインターフェイスを設定するインターフェイス記述を、前記ハードウェア設計記述及び前記アサーションに基づいて生成するインターフェイス記述生成部をさらに具備することを特徴とする請求項１記載のデジタル回路検証装置。
【請求項４】
請求項２に記載のデジタル回路検証装置に入力される前記アサーションのデータ構造であって、
前記検証プログラム解釈部に前記共有記憶部へアクセスさせる命令、
前記検証プログラム解釈部に前記出力部への出力を行わせる命令、
前記検証プログラム解釈部に前記変数実体判定部を駆動させる命令、
前記検証プログラム解釈部に前記変数読込部を駆動させる命令、
前記検証プログラム解釈部に前記変数書込部を駆動させる命令、
のいずれか又は任意の組み合わせからなり、前記時相論理式が表現する命題が真になったとき実行される検証プログラムと、前記時相論理式の組の集合を表現するアサーションのデータ構造。
【請求項５】
検証対象とするデジタル回路のハードウェア設計記述の論理シミュレーションを行うと共に前記デジタル回路のハードウェア設計記述が時相論理式を満たしているかどうかを判定するハードウェア設計記述シミュレータと協働し、前記時相論理式、及び前記時相論理式が表現する命題が真になったときに実行すべき検証プログラムの組の集合からなるアサーションを入力として前記デジタル回路の機能を検証するデジタル回路検証装置によるデジタル回路検証方法であって、
検証プログラム選択部が、前記ハードウェア設計記述シミュレータから前記時相論理式の判定結果を受け取り、前記判定結果に対応する検証プログラムを選択するステップと、
共有記憶部が、前記集合における検証プログラムの全ての間で共有される値を記憶するステップと、
前記検証プログラム選択部により選択された検証プログラムを、前記共有記憶部に記憶された値を参照しながら検証プログラム解釈部が解釈し、前記共有記憶部への値の書込を行うステップと、
前記検証プログラム解釈部による前記検証プログラムの解釈結果を前記デジタル回路の検証結果として出力部が出力するステップと、を具備することを特徴とするデジタル回路検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ＬＳＩ設計などデジタル回路を主とするシステムの設計記述の検証に関する。
【背景技術】
【０００２】
デジタル回路を主とするシステムの設計において、回路の構成要素をＩＰ（Ｉｎｔｅｌｌｅｃｔｕａｌ  Ｐｒｏｐｅｒｔｙ；知識資産）としてモジュール化する方法が用いられて久しい。ＩＰは以下の２つの特徴を持つ。
【０００３】
・階層構造。ＩＰは他のＩＰを組み合わせて構成することができる。これにより、回路の構成要素を抽象化の度合いに応じてモジュール化することができる。ただし、ＩＰの階層構造は設計仕様の変更により変化しうる。
【０００４】
・再利用性。ＩＰは入出力の信号が出ているブラックボックスとして扱える。これにより、一度記述したＩＰを別の回路の設計に再利用することができる。
【０００５】
近年、ＩＰの設計仕様を形式的に記述したアサーションを用いてＩＰを検証する方法が盛んに行われている。アサーションはＩＰの中の信号変化の履歴に関する時相論理式や正規表現（以下まとめて「時相論理式」と呼ぶ）をベースとしたプロパティ記述言語によって記述される。従来のプロパティ記述言語にはＰＳＬ（Ｐｒｏｐｅｒｔｙ  Ｓｐｅｃｉｆｉｃａｔｉｏｎ  Ｌａｎｇｕａｇｅ）、ＳＶＡ（Ｓｙｓｔｅｍ  Ｖｅｒｉｌｏｇ  Ａｓｓａｔｉｏｎ）などが知られている。アサーションを元に、ＩＰの設計を検証したり、ＩＰを正しく利用しているかどうかの検証をすることができる（例えば、特許文献１、２参照。）。アサーションは、対象としているＩＰ自身に埋め込まれる（もしくは添付される）形で記述される。これにより、ＩＰが自分自身を検証するためＩＰの信頼性が向上し、設計プロセスの効率化が図られる。具体例としては、以下のような利点が生まれる。
【０００６】
・テストベクトルの不足などによりＩＰがバグを持ったまま単体テストを通過してしまい、統合テストで初めてバグが発生した場合、どのＩＰがバグを持っているのかわからなくなりがちであったが、単体テストの内容をアサーションとして記述しておくことで、統合テスト時でも単体テストを実行できる。
【０００７】
・アサーションをＩＰの外に置く場合、ＩＰを再利用したり階層構造が変化したりするたびにアサーションの記述を更新しなければならなかったが、この手間がなくなる。
【０００８】
また、アサーションに関する注意事項として、以下が挙げられる。
【０００９】
・アサーションを記述する際は、そのＩＰがどこでどのように使用されるかの仮定を置くことはできない。すなわち、アサーションは自身が埋め込まれているＩＰの中の信号変化しか指示してはならない。実際、従来のプロパティ記述言語は、他のＩＰの中の信号を指示することを不可能であるように設計されている。なぜならば、アサーションが他のＩＰの信号変化を指示した場合、そのアサーションのＩＰは他の特定のＩＰと併せて使われることを仮定してしまい、また、他のＩＰの指示をする場合、ＩＰの階層構造を持って指示することになるため、ＩＰの階層構造も仮定してしまう。
【００１０】
・すでに設計記述のあるＩＰにアサーションを記述する際、アサーションを記述するためにそのＩＰや他のＩＰの設計記述を変更してはならない。ＩＰを回路に落とす段階になるとアサーションは取り外されるものである。アサーションを取り外したときにＩＰの設計記述が不自然であると、回路への変換の際の最適化を阻害することがある。回路に落とす段階でＩＰに加えた変更を戻してしまうと、アサーションによって記述された性質が保証されなくなる。
【特許文献１】特開２００６−９９５１８号公報
【特許文献１】特開２００７−１１４６７号公報
【発明の開示】
【発明が解決しようとする課題】
【００１１】
従来のアサーションでは、ＩＰの中の信号変化の履歴に関する時相論理式として記述していた。このアサーションを検証する場合、シミュレータが回路全体の設計記述を論理シミュレーションし、時相論理式判定装置が、アサーションとして記述された時相論理式が表現する命題を判定し、検証装置は、時相論理式判定装置の結果が真になった場合、ＩＰがアサーションを満たしていないものとしてエラーを報告していた。
【００１２】
しかしこのような方法では、指定した信号変化の発生順序で表現できる程度の仕様しか表現できず、アルゴリズムのような高度な仕様をアサーションとして記述することはできなかった。また、アサーションは自身が埋め込まれているＩＰの中の信号変化しか指示できないため、ＩＰ間にまたがる仕様、ＩＰとＩＰを組み合わせたときに生じる性質を記述することはできなかった。
【００１３】
本発明は、従来のアサーションでは記述できなかったアルゴリズムのような高度な仕様や、ＩＰ間にまたがる仕様を記述できるプロパティ記述言語で書かれたアサーションを処理するデジタル回路検証のための装置及び方法を提供することを目的とする。
【課題を解決するための手段】
【００１４】
本発明の一観点に係るデジタル回路検証装置は、検証対象とするデジタル回路のハードウェア設計記述の論理シミュレーションを行うと共に前記デジタル回路のハードウェア設計記述が時相論理式を満たしているかどうかを判定するハードウェア設計記述シミュレータと協働し、前記時相論理式、及び前記時相論理式が表現する命題が真になったときに実行すべき検証プログラムの組の集合からなるアサーションを入力として前記デジタル回路の機能を検証するデジタル回路検証装置であって、前記ハードウェア設計記述シミュレータから前記時相論理式の判定結果を受け取り、前記判定結果に対応する検証プログラムを選択する検証プログラム選択部と、前記集合における検証プログラムの全ての間で共有される値を記憶する共有記憶部と、前記検証プログラム選択部により選択された検証プログラムを前記共有記憶部に記憶された値を参照しながら解釈し、前記共有記憶部への値の書込を行う検証プログラム解釈部と、前記検証プログラム解釈部による前記検証プログラムの解釈結果を前記デジタル回路の検証結果として出力する出力部と、を具備することを特徴とする。
【発明の効果】
【００１５】
本発明によれば、高度な仕様や、ＩＰ間にまたがる仕様を記述できるプロパティ記述言語で書かれたアサーションを処理するデジタル回路検証のための装置、方法、及びプログラムを提供できる。
【発明を実施するための最良の形態】
【００１６】
以下、添付図面を参照しながら本発明を実施するための最良の形態について説明する。
【００１７】
本発明の実施形態では、時相論理式と、その時相論理式が表現する命題が真になったときに取るべき動作を記述した検証プログラムの組の集合としてアサーションを定義し、このアサーションを埋め込んだＩＰを含む回路全体の設計記述を入力とする。そして、従来のシミュレータを用いて設計記述を論理シミュレーションし、従来の時相論理式判定装置を用いて、アサーションの一部として記述された時相論理式が表現する命題を判定する。
【００１８】
以下に説明する本発明の実施形態に係るデジタル回路検証装置は、時相論理式判定装置の判定結果が真になった場合に、検証プログラム解釈部を駆動し、真になった時相論理式と対になっている検証プログラムを実行する。検証プログラム解釈部は、全ての検証プログラム間で共有する値を保持する共有記憶部を駆動しながら検証プログラムを実行する。以上の一連の機構により、アルゴリズムのような高度な仕様や、ＩＰ間にまたがる仕様をアサーションとして記述できるプロパティ記述言語を処理する装置を提供する。
【００１９】
（第１の実施形態）
第１の実施形態はＩＰ間にまたがる仕様のアサーション記述及びその検証に関する。
【００２０】
図１は、実施形態に係るデジタル回路検証装置の構成を示すブロック図である。デジタル回路検証装置１０１は、検証プログラム選択部１０２と、検証プログラム読取部１０３と、共有記憶部１０４と、検証プログラム解釈部１０５と、検証結果表示・記憶部１０６を備える。また、変数実体判定部１０７と、変数読込部１０８と、変数書込部１０９を備える。
【００２１】
以下、図１に示す構成に基づく処理の流れを説明する。
【００２２】
まず、アサーションが埋め込まれたハードウェア設計記述１１０から、従来の回路記述であるハードウェア設計記述（以下、「設計記述」という）１１１、時相論理式１１２、及び検証プログラム１１３の組の集合を得る。設計記述１１１及び時相論理式１１２は既存のハードウェア設計記述シミュレータ（以下、「設計記述シミュレータ」という）１１４へ入力される。設計記述シミュレータ１１４内のハードウェア設計記述解釈部１１５は、設計記述１１１と、デジタル回路への入力であるテストベンチ１１６を入力し、デジタル回路の出力であるテストベンチ実行結果１２０と、デジタル回路の中の信号が示す値の変化の履歴を示す信号変化履歴１１７を出力する。時相論理式判定部１１８は、時相論理式１１２と信号変化履歴１１７を入力とし、信号変化履歴１１７上で時相論理式１１２が真になる時点では真を、そうでない時点では偽を出力する。
【００２３】
本実施形態に係るデジタル回路検証装置１０１は、検証プログラム１１３の集合と、時相論理式判定部１１８の判定結果とを入力とする。検証プログラム選択部１０２は、検証プログラム１１３の集合と前記判定結果を入力し、前記判定結果が真である時相論理式１１２に対応する検証プログラム１１３を選択する。選択された検証プログラム１１３は検証プログラム読取部１０３によって読み取られる。このとき、検証プログラム１１３の実行を高速化するために検証プログラム１１３の変換や解析を行ってもよい。
【００２４】
検証プログラム解釈部１０５は、読み取られた検証プログラム１１３に含まれている命令を実行する。検証プログラム１１３は、通常の算術命令や制御構造のほか、後述する共有記憶部１０４の中の値を読み書きする命令と、設計記述１１１の中の信号の値を読み書きする命令の任意の組み合わせからなる。そのため検証プログラム解釈部１０５は、後述する共有記憶部１０４とハードウェア設計記述解釈部１１５に対して適宜読み書きを行う。
【００２５】
共有記憶部１０４は、検証プログラム１１３が実行中に必要な記憶領域として使用される。共有記憶部１０４は値を保持するセルの有限な集合である。セルには一意な名前を振ることができる。この共有記憶部１０４が本実施形態においてもっとも重要な構成要素であり、この共有記憶部１０４を計算領域として使うことでアルゴリズムのシミュレートが可能になる。また、検証プログラム１１３間で通信を行うための同期信号として使うことで複数アサーションの協調による検証が可能になる。
【００２６】
本実施形態では、検証プログラム１１３は変数を持ち、変数の実体は共有記憶部１０４の中の値か設計記述１１１の中の値のいずれかであるとする。変数の実体が共有記憶部１０４の中の値であるとき、その変数を「共有変数」と呼ぶ。変数の実体が設計記述１１１の中の値であるとき、その変数を「信号変数」と呼ぶ。これらによって、共有記憶部１０４への読み書きの命令も設計記述１１１の中の信号の値の読み書きの命令も、変数への読み書きの命令として統一して記述することができる。これを実現するために、図１に示すように変数実体判定部１０７、変数読込部１０８、変数書込部１０９を持つ。
【００２７】
変数実体判定部１０７は、入力された変数が共有変数であるか信号変数であるかを判定する。この判定は、変数の宣言、代入の流れ、変数が使われている文脈などを元に行われる。基本ブロック解析やｄｅｆ−ｕｓｅ解析など、検証プログラム１１３を静的解析する場合は、この変数実体判定部１０７で行ってもよいが、実行中に解析結果が変化しないことがわかっている場合は、効率を上げるために検証プログラム読取部１０３であらかじめ解析しておいてもよい。
【００２８】
変数読込部１０８は、変数実体判定部１０７の判定結果が共有変数であった場合は、共有記憶部１０４の中の値を読み取り、検証プログラム１１３へ伝える。判定結果が信号変数であった場合は、信号記憶部１１９に記憶されている、設計記述１１１の中の値を読み取り、検証プログラム解釈部１０５へ伝える。共有記憶部１０４の中の値を読み取る場合は共有記憶部１０４へ問い合わせ、信号記憶部１１９（設計記述）の中の値を読み取る場合はハードウェア設計記述解釈部１１５へ問い合わせる。
【００２９】
また変数読込部１０８は、変数読込部１０８と同様に変数実体判定部１０７の判定結果を元に、検証プログラム解釈部１０５から受け取った値を共有記憶部１０４の中又は設計記述１１１の中に代入する。共有記憶部１０４の中に代入場合は共有記憶部１０４へ問い合わせ、設計記述１１１の中に代入する場合はハードウェア設計記述解釈部１１５へ問い合わせる。
【００３０】
検証プログラム解釈部１０５は、変数への読み書きの命令を実行するとき、変数実体判定部１０７に変数を入力する。実行する命令が書き込み命令であるときは、書き込む値を変数書込部１０９に書き込む値を与える。実行する命令が読み込み命令であるときは、変数読込部１０８が値を読み込むのを待ち、読み込んだ値を得る。
【００３１】
このように、本発明の第１の実施形態においては、時相論理式１１２がマッチしたタイミングで実行すべき命令を検証プログラム１１３として指定できるので、従来のアサーションより柔軟かつ高度なレベルで仕様を記述することができるという効果がある。
【００３２】
（具体例１）
以下、具体的なモチーフを用いて本実施形態の動作を説明する。
【００３３】
図２は、画像処理ＩＰ２００、ボタン２０１、画像処理制御ＩＰ２０２、及びメモリＩＰ２０３からなる、画像の平滑化を行う回路の構成を示している。
【００３４】
画像処理ＩＰ２００は、開始要求信号を受けたら、メモリＩＰ２０３から入力画像を少しずつ読み込み、読み込んだ部分に対して平滑化（ぼかし）を行ったものを出力し、終了通知信号を立て、次の開始要求信号を待つ。画像処理ＩＰ２００はその中にｐｒｏｃ＿ｓｔａｔｅという名の信号を持ち、これが画像処理制御ＩＰ２０２の状態を表現している。図３は画像処理ＩＰ２００内部の状態遷移図である。開始要求信号を待っている状態３００が｀ＩＤＬＥであり、平滑化処理を行っている状態３０１が｀ＢＵＳＹである。
【００３５】
ボタン２０１はユーザからの入力を受け付ける。
【００３６】
画像処理制御ＩＰ２０２は、ボタン２０１が押されるのを監視し、ボタン２０１が押されたら画像処理ＩＰ２００へ開始要求信号を送り、画像処理ＩＰ２００から終了通知信号を待った後、次にボタン２０１が押されるのを待つ。画像処理制御ＩＰ２０２はその中にｃｎｔｌ＿ｓｔａｔｅという名の信号を持ち、これが画像処理制御ＩＰ２０２の状態を表現している。図４は画像処理制御ＩＰ２０２内部の状態遷移図である。ボタン２０１が押されるのを待っている状態４００が｀ＩＮＰＵＴであり、画像処理ＩＰ２００からの終了通知信号を待っている状態４０１が｀ＷＡＩＴである。
【００３７】
メモリＩＰ２０３は、平滑化を行う前の画像と、平滑化を行った後の画像を保持する。
【００３８】
この回路に対し、「画像処理ＩＰ２００と画像処理制御ＩＰ２０２はデッドロックしない」、すなわち、「画像処理ＩＰ２００と画像処理制御ＩＰ２０２が同時にお互いを待ち合う状態にならない」という仕様をアサーションとして記述する場合を考える。
【００３９】
ここで、画像処理ＩＰ２００の「待ち状態」を、開始要求信号を待っている状態のことと定義し、画像処理制御ＩＰ２０２の「待ち状態」を、画像処理ＩＰ２００からの終了通知信号を待っている状態のことと定義する。
【００４０】
「デッドロックしない」という仕様は、ＩＰ間をまたがる仕様であり、従来のアサーションからは参照できなかった。なぜならば、アサーションとして記述する場合、画像処理ＩＰ２００が待ち状態かどうか、画像処理制御ＩＰ２０２が待ち状態かどうか、の両方を観測する必要がある。しかし、ＩＰが待ち状態かどうかを判定するにはそのＩＰの状態を表す信号を参照しなければならないが、そのような信号は一般的にそのＩＰの中で定義されているため参照できなかった。
【００４１】
以下、この仕様をモチーフとした場合の動作を説明する。
【００４２】
本発明を適用する際、ユーザはまず図５及び図６のような２つのアサーションを記述する。ここで使われている文法はあくまで一例であり、本発明は特定の文法に限定されない。時相論理式とそれに対応する検証プログラムを記述できればよい。
【００４３】
図５のアサーションは、画像処理ＩＰ２００に埋め込まれている。このアサーションは時相論理式１１２と検証プログラムの組を２つ持つ。１つ目は、画像処理ＩＰ２００が開始要求信号を待っている状態を表す時相論理式
｛ｐｒｏｃ＿ｓｔａｔｅ  ＝＝  ｀ＩＤＬＥ｝
と、それが真の時に実行すべき検証プログラム
ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｔｒｕｅ；
ｉｆ（ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ）  ｅｒｒｏｒ（）；
である。前述の通り、ｐｒｏｃ＿ｓｔａｔｅは画像処理ＩＰ２００の中の信号の名前であり、画像処理ＩＰ２００の状態を表す。すなわち、変数ｐｒｏｃ＿ｓｔａｔｅが｀ＩＤＬＥであるとき、画像処理ＩＰ２００は待ち状態である。変数ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄと変数ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄは共有記憶部１０４の中の値を指す。変数名に「＿ｓｈａｒｅｄ」をつけているのはわかりやすさのためであり、このように命名しなければならないわけではない。この検証プログラムはｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄに真を代入し、さらにｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄを読み出し、それが真であったとき関数ｅｒｒｏｒを呼び出してエラーを報告するプログラムである。また、２つ目は、変数ｐｒｏｃ＿ｓｔａｔｅが｀ＩＤＬＥでないという時相論理式と、ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄに偽を代入するという検証プログラムの組である。以上を総合すると、図５のアサーションは、画像処理ＩＰ２００が待ち状態であるかどうかを共有変数ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄに反映し、画像処理ＩＰ２００が待ち状態であるとき共有変数ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄが真であることはない、という仕様を表現している。
【００４４】
図６のアサーションは、逆に、画像処理制御ＩＰ２０２について同様のアサーションを記述している。すなわち、画像処理制御ＩＰ２０２が待ち状態であるかどうかを共有変数ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄに反映し、画像処理制御ＩＰ２０２が待ち状態であるとき共有変数ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄが真であることはない、という仕様を表現している。
【００４５】
これら２つのアサーションによって、「画像処理ＩＰ２００が待ち状態であるときは画像処理制御ＩＰ２０２が待ち状態ではなく、かつ、画像処理制御ＩＰ２０２が待ち状態であるときは、画像処理ＩＰ２００が待ち状態でない」という仕様を表現することができる。
【００４６】
以下、この２つのアサーションをどのように処理するかについて説明する。
【００４７】
まず、設計記述シミュレータ１１４は、回路全体の設計記述と、回路へのテストベンチと、図５と図６の時相論理式（ここでは計４つ）を入力し、テストベンチ実行結果と時相論理式の判定結果を出力する。この具体例では、図５と図６の検証プログラム（ここでは計４つ）と、設計記述シミュレータ１１４が出力した時相論理式の判定結果を入力する。
【００４８】
ここで、画像処理制御ＩＰ２０２がボタン２０１が押されるのを待っている状態（「待ち状態」ではない）であり、画像処理ＩＰ２００が待ち状態である状況を考える。このとき、ｃｎｔｌ＿ｓｔａｔｅは｀ＩＮＰＵＴであり、ｐｒｏｃ＿ｓｔａｔｅは｀ＩＤＬＥである。そのため、４つの時相論理式はそれぞれ図７のように判定される。
【００４９】
検証プログラム選択部１０２は、この判定結果を入力し、真である時相論理式
｛ｐｒｏｃ＿ｓｔａｔｅ  ＝＝  ｀ＩＤＬＥ｝
と
｛ｃｎｔｌ＿ｓｔａｔｅ  ！＝  ｀ＷＡＩＴ｝
に対応する検証プログラムである
ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｔｒｕｅ；
ｉｆ（ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ）  ｅｒｒｏｒ（）；
と、
ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｆａｌｓｅ；
とを選択する。
【００５０】
検証プログラム読取部１０３は、前記２つの検証プログラムを読み取り、検証プログラム解釈部１０５へ送る。検証プログラム解釈部１０５は２つの検証プログラムを実行する。
【００５１】
ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｆａｌｓｅ；
では、検証プログラム解釈部１０５は変数実体判定部１０７にｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄを入力する。変数実体判定部１０７はｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄが共有変数であると判定し出力する。検証プログラム解釈部１０５は変数書込部１０９に偽の値を入力する。変数書込部１０９は変数実体判定部１０７の判定結果から、共有記憶部１０４のｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄを保持するセルに対して偽の値を書き込む。以上によって、共有変数ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄに偽を代入する。同様に
ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｔｒｕｅ；
では共有変数ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄに真を代入する。
【００５２】
ｉｆ（ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ）  ｅｒｒｏｒ（）；
では、検証プログラム解釈部１０５は変数実体部にｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄを入力する。変数実体判定部１０７はｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄが共有変数であると判定し出力する。変数読込部１０８は変数実体判定部１０７の判定結果から、共有記憶部１０４のｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄを保持するセルから値を読み出す。以上によって共有変数ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄを読み込む。ここでは偽が読み込まれるため、関数ｅｒｒｏｒは実行されない。
【００５３】
次に、画像処理ＩＰ２００が平滑化処理をしており、画像処理制御ＩＰ２０２が終了通知信号を待っている状態である状況を考える。このとき、ｃｎｔｌ＿ｓｔａｔｅは｀ＷＡＩＴであり、ｐｒｏｃ＿ｓｔａｔｅは｀ＢＵＳＹである。そのため、４つの時相論理式はそれぞれ図８のように判定される。
【００５４】
検証プログラム選択部１０２はこの判定結果を入力し、真である時相論理式
｛ｐｒｏｃ＿ｓｔａｔｅ  ！＝  ｀ＩＤＬＥ｝
と
｛ｃｎｔｌ＿ｓｔａｔｅ  ＝＝  ｀ＷＡＩＴ｝
に対応する検証プログラムである
ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｆａｌｓｅ；
と
ｃｔｒｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｔｒｕｅ；
ｉｆ（ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ）  ｅｒｒｏｒ（）；
とを選択する。
【００５５】
検証プログラム読取部１０３は、前記２つの検証プログラムを読み取り、検証プログラム解釈部１０５へ送る。検証プログラム解釈部１０５は変数実体判定部１０７、変数読込部１０８、変数書込部１０９を利用しながら２つの検証プログラムを実行する。
【００５６】
ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｆａｌｓｅ；
では、共有変数ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄに偽を代入する。
【００５７】
ｃｔｒｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｔｒｕｅ；
では、共有変数ｃｔｒｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄに真を代入する。
【００５８】
ｉｆ（ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ）  ｅｒｒｏｒ（）；では共有変数ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄを読み込む。ここでは偽が読み込まれるため、関数ｅｒｒｏｒは実行されない。
【００５９】
最後に、画像処理ＩＰ２００も画像処理制御ＩＰ２０２も待ち状態である状況を考える。このとき、ｃｎｔｌ＿ｓｔａｔｅは｀ＷＡＩＴであり、ｐｒｏｃ＿ｓｔａｔｅは｀ＩＤＬＥである。そのため、４つの時相論理式はそれぞれ図９のように判定される。
【００６０】
検証プログラム選択部１０２はこの判定結果を入力し、真である時相論理式
｛ｐｒｏｃ＿ｓｔａｔｅ  ＝＝  ｀ＩＤＬＥ｝
と
｛ｃｎｔｌ＿ｓｔａｔｅ  ＝＝  ｀ＷＡＩＴ｝
に対応する検証プログラムである
ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｔｒｕｅ；
ｉｆ（ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ）  ｅｒｒｏｒ（）；
と
ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｔｒｕｅ；
ｉｆ（ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ）  ｅｒｒｏｒ（）；
とを選択する。
【００６１】
検証プログラム読取部１０３は、前記２つの検証プログラムを読み取り、検証プログラム解釈部１０５へ送る。検証プログラム解釈部１０５は変数実体判定部１０７、変数読込部１０８、変数書込部１０９を利用しながら２つの検証プログラムを実行する。
【００６２】
ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｔｒｕｅ；
では、共有変数ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄに真を代入する。
【００６３】
ｉｆ（ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ）  ｅｒｒｏｒ（）；
では共有変数ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄを読み込む。この値は本状況に到達するまでの過程に依存する。仮に真が読み込まれた場合は関数ｅｒｒｏｒを実行し、偽が読み込まれた場合は何もしない。
【００６４】
ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄ  ＝  ｔｒｕｅ；
では、共有変数ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄに真を代入する。
【００６５】
ｉｆ（ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄ）  ｅｒｒｏｒ（）；
では共有変数ｃｎｔｌ＿ｓｔａｔｅ＿ｓｈａｒｅｄを読み込む。ここでは真が読み込まれるため、関数ｅｒｒｏｒは実行されない。従って、共有変数ｐｒｏｃ＿ｓｔａｔｅ＿ｓｈａｒｅｄの値が真であるか偽であるかに関わらず、関数ｅｒｒｏｒが実行される。
【００６６】
関数ｅｒｒｏｒは検証プログラム解釈部１０５の組み込み関数であり、実行された場合の挙動は任意であるが、通常の場合は、検証結果表示・記憶部１０６に対してエラーログを出力したり、シミュレーションを異常終了させたりすることが考えられる。言うまでもないが、本発明はｅｒｒｏｒという関数名に限定されない。
【００６７】
このように、この具体例１においては、「画像処理ＩＰ２００と画像処理制御ＩＰ２０２がデッドロックしない」という仕様を記述したアサーションを元に、各ＩＰの設計記述１１１がこの仕様を満たしているかどうかを検証することができるという効果がある。
【００６８】
（具体例２）
上述した具体例１のアサーションは、判定結果が出るたびに必ず検証プログラムを実行していたため、シミュレーションプロセスに時間がかかる可能性がある。図１０と図１１に示すアサーションであれば、ｐｒｏｃ＿ｓｔａｔｅが変化したときとｃｎｔｌ＿ｓｔａｔｅが変化したときのみ検証プログラムを実行するため、高速である。
【００６９】
（第２の実施形態）
次に、本発明の第２の実施形態について説明する。この実施形態は、従来のアサーションでは記述できなかったアルゴリズムのような高度な仕様の記述及び検証に関する。システムの基本構成とモチーフは第１の実施形態と同じである。ただし、画像処理ＩＰ２００の入出力の動作を細かく規定する。画像処理ＩＰ２００は信号ｒｄを立て、信号ａｄｄｒにアドレスを設定することで、メモリＩＰ２０３から指定したアドレスのデータ（入力画像の一部）を読み込む。データは信号ｄａｔａから参照する。画像処理ＩＰ２００は、信号ｗｒを立て、信号ａｄｄｒにアドレスを設定し、信号ｄａｔａにデータ（出力画像の一部）を設定することで、メモリＩＰ２０３の指定したアドレスにデータを書き込む。また、処理終了信号はａｃｋである。
【００７０】
例として、「画像処理ＩＰ２００が入力した画像を平滑化アルゴリズムで処理した画像を出力する」という仕様をアサーションとして記述する場合を考える。従来のアサーションでは時相論理式による記述であったため、究極的には、指定したイベントの列が発生すること、又は発生しないことしか記述できず、平滑化アルゴリズムを表現することはできなかった。本実施形態によれば、検証プログラムの中に平滑化アルゴリズムを記述することで容易に表現ができる。
【００７１】
図１２は、「画像処理ＩＰ２００が入力した画像を平滑化アルゴリズムで処理した画像を出力する」という仕様を表現するアサーションである。このアサーションは画像処理ＩＰ２００に埋め込まれている。
【００７２】
図１２のアサーションは時相論理式と検証プログラムの３つの組からなる。
【００７３】
１つ目は、信号ｒｄが立ったとき、すなわち入力が発生したときを表現する時相論理式と、
ｓｒｃＭｅｍ［ａｄｄｒ］＝ｄａｔａ；
という検証プログラムである。変数ｓｒｃＭｅｍは共有記憶部１０４の中で保存されている値である。変数ａｄｄｒと変数ｄａｔａは、それぞれ画像処理ＩＰ２００の中の同名の信号を表す。この検証プログラムは、入力が発生した時点で信号ａｄｄｒとｄａｔａが表す値を、ｓｒｃＭｅｍが示す共有記憶部１０４のセルに記憶させる。すなわち、入力画像の断片を共有記憶部１０４に蓄積していく。
【００７４】
２つ目は、出力が発生した時点で１つ目と同様のことを共有変数ｄｓｔＭｅｍに記憶していく。すなわち、出力画像の断片を共有記憶部１０４に蓄積していく。
【００７５】
３つ目は、信号ａｃｋが立ったとき、すなわち処理が終了したときを表現する時相論理式と、
ｉｆ（ｂｌｕｒ（ｓｒｃＭｅｍ）  ！＝  ｄｓｔＭｅｍ）  ｅｒｒｏｒ（）；
という検証プログラムである。処理が終了した時点であるため、共有変数ｓｒｃＭｅｍとｄｓｔＭｅｍにはそれぞれ入力画像の全体と出力画像の全体が記憶されている。関数ｂｌｕｒは同アサーション内に定義されている関数であり、画像を受け取り、平滑化アルゴリズムを実行し、平滑化した画像を返す。よってこの検証プログラムは、入力画像を平滑化し、出力画像と一致するかどうかを判定し、一致しなかった場合は関数ｅｒｒｏｒを実行する。
【００７６】
本実施形態はこのアサーションを扱うことができる。図１３は、図１２のアサーションと設計記述１１１を本実施形態で検証した場合の動作図である。各部の詳細な動きについての説明は省略する。
【００７７】
（第３の実施形態）
第３の実施形態は、設計記述シミュレータ１１４を使うために必要なインターフェイス記述の自動生成に関する。第１、第２の実施形態では、デジタル回路検証装置１０１内の検証プログラム選択部１０２は、時相論理式の判定結果を設計記述シミュレータ１１４から読み込むものとして説明した。しかし実際にこれを実現するためには、設計記述シミュレータ１１４と外部装置との通信の仕方、すなわち、時相論理式の判定結果をデジタル回路検証装置１０１に対して入力する、という指示であるインターフェイス記述を設計記述シミュレータ１１４に与える必要がある。インターフェイス記述をアサーションを記述する際に合わせて直接手で記述してもよいが、アサーションを記述するごとにインターフェイス記述を記述するのは煩雑である。そこで本実施形態では、デジタル回路検証装置１０１は、アサーションの記述からインターフェイス記述を自動生成するインターフェイス記述生成部１６０を備えている。
【００７８】
以下、設計記述言語としてＶｅｒｉｌｏｇ  ＨＤＬ、プロパティ記述言語としてＰＳＬを用いて説明する。ただし本発明はこれらに限定されず、同様の機能を提供する設計記述言語とプロパティ記述言語でも実施可能である。また、設計記述シミュレータ１１４が同様の機能を独自に提供している場合も実施可能である。
【００７９】
Ｖｅｒｉｌｏｇ  ＨＤＬには外部装置が通信するためのインターフェイス規格であるＰＬＩ（Ｐｒｏｇｒａｍｍｉｎｇ  Ｌａｎｇｕａｇｅ  Ｉｎｔｅｒｆａｃｅ）がある。ＰＬＩは、Ｃ言語プログラムと、Ｖｅｒｉｌｏｇ  ＨＤＬの任意の時点から前記Ｃ言語プログラムを呼び出す指示の組からなり、指定したイベントが起きたときに任意のＣ言語のプログラムを設計記述シミュレータ１１４に実行させることができる。この命令を適切に与えることで、設計記述１１１の中の信号の値を外部装置に通知させることができる。また、外部装置から設計記述シミュレータ１１４の内部状態へアクセス要求が来たときに応えさせることもできる。この命令を適切に与えることで、外部装置から設計記述１１１の中の信号の値を読み書きできるようにすることができる。
【００８０】
図１４はＰＬＩ記述の例を表す図である。Ｃ言語の関数ｆｏｏの定義と、この関数を呼び出す指示
＄ｆｏｏ；
を含むＶｅｒｉｌｏｇ  ＨＤＬの記述の組からなる。すなわちこのＰＬＩ記述は、信号ｆｏｏが真になったとき、Ｃ言語の関数ｆｏｏを呼び出すという記述である。これを用いて、Ｃ言語のコードから外部装置と通信を行えばよい。尚、本発明はその際の通信手段を特に限定しない。例えば、外部装置が同じコンピュータ上で動くプログラムである場合は、共有メモリやソケットなどを用いればよい。
【００８１】
ＰＳＬでは、ＰＳＬエンドポイントと呼ばれる、時相論理式の判定結果を設計記述１１１から参照するためのインターフェイス規格がある。図１５はＰＳＬエンドポイント宣言の例を表す図である。これを宣言すると、
｛ｘ＝１｝
という時相論理式の成否を、ｆｏｏという擬似的な信号として設計記述１１１から参照できる。
【００８２】
以上のように、ＰＳＬエンドポイント宣言を使うと時相論理式の判定結果を設計記述１１１から信号として参照でき、ＰＬＩ記述を使うと設計記述１１１の中の信号を外部装置へ伝えることができる。従って、この２つを組み合わせることで時相論理式の判定結果を外部装置へ伝えることができる。図１６は、ＰＬＩ記述とＰＳＬエンドポイント宣言を組み合わせることで、時相論理式の判定結果を外部装置へ伝えるように構成された設計記述シミュレータ１１４のブロック図である。
【００８３】
インターフェイス記述生成部１６０は、アサーションを含む設計記述１１１を入力し、アサーションからＰＬＩ記述とＰＳＬエンドポイント宣言の組の集合を生成し、ＰＬＩ記述とＰＳＬエンドポイント記述を含んだ設計記述１１１を出力する。
【００８４】
具体的な生成手段は以下のようになる。
【００８５】
・アサーション中の時相論理式すべてについて一意な名前を割り当てる。
【００８６】
・割り当てた名前を用いて、すべての時相論理式についてＰＳＬエンドポイント宣言を生成する。これによって、時相論理式が真になった瞬間を真偽値として返す擬似的な信号を作ることができる。
【００８７】
・ＰＳＬエンドポイント宣言によって生成された擬似的な信号を監視し、デジタル回路検証装置１０１へ擬似的な信号の値を通知するＰＬＩ記述を生成する。これによってデジタル回路検証装置１０１は各時相論理式の表す命題の真偽を参照することができる。第１の実施形態で示した図５のアサーションから生成したインターフェイス記述の例を図１７に示す。
【００８８】
図１８は、以上のようなインターフェイス記述生成部１６０を具備し、アサーションを含む設計記述１１１からアサーションの検証を行うように構成されたデジタル回路検証装置１８０を示すブロック図である。これによって、ユーザは検証時に設計記述シミュレータ１１４に与えるインターフェイス記述を手動で生成する必要がなくなる。
【００８９】
以上説明した実施形態によれば、高度な仕様や、ＩＰ間にまたがる仕様をアサーションとして記述することにより、ＩＰが自分自身を詳細に検証することからＩＰの信頼性が向上し、設計プロセスを効率的に実行することができる。
【００９０】
以下、実施形態において容易に改良が可能な点を挙げる。
【００９１】
・アサーションの再利用。アサーションとして記述したい仕様には頻出形があると考えられる。例えば実施形態で説明したデッドロックフリーという仕様は、実施形態の画像処理ＩＰ２００と画像処理制御ＩＰ２０２以外でも記述したくなることが頻出する。そのため、アサーションの再利用性を高める拡張が考えられる。具体的には、検証プログラムの部分だけ定義したテンプレートを用意し、時相論理式の指定だけを付け足して再利用することができる。これはオブジェクト指向プログラミングの概念の一つである継承を検証プログラム記述言語に導入することで自明に解決できる。
【００９２】
・固有記憶部の設置。実施形態では、設計記述１１１の中の信号を表す変数、全検証プログラムで共有される変数しか扱っていないが、ローカル変数を記述できるよう、各検証プログラムに固有の記憶部を設置することが考えられる。
【００９３】
本発明は上記実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、上記実施形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成できる。例えば、実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。さらに、異なる実施形態にわたる構成要素を適宜組み合わせてもよい。
【図面の簡単な説明】
【００９４】
【図１】実施形態に係るデジタル回路検証装置の構成を示すブロック図
【図２】画像の平滑化を行う回路の構成図
【図３】画像処理ＩＰの状態遷移図
【図４】画像処理制御ＩＰの状態遷移図
【図５】デッドロックしないという性質を記述した画像処理ＩＰ側のアサーションの図
【図６】デッドロックしないという性質を記述した画像処理制御ＩＰ側のアサーションの図
【図７】画像処理ＩＰが待ち状態の時の４つの時相論理式の判定結果を表す図
【図８】画像処理制御ＩＰが待ち状態の時の４つの時相論理式の判定結果を表す図
【図９】デッドロック時の４つの時相論理式の判定結果を表す図
【図１０】デッドロックしないという性質を記述した画像処理ＩＰ側の別のアサーションの図
【図１１】デッドロックしないという性質を記述した画像処理制御ＩＰ側の別のアサーションの図
【図１２】平滑化アルゴリズムの仕様を記述したアサーションの図
【図１３】平滑化アルゴリズムの仕様を記述したアサーションを用いた検証を表す図
【図１４】ＰＬＩ記述の例を表す図
【図１５】ＰＳＬエンドポイント宣言の図
【図１６】時相論理式の判定結果を外部装置へ伝える設計記述シミュレータのブロック図
【図１７】インターフェイス記述の例を表す図
【図１８】インターフェイス記述生成部を持つデジタル回路検証装置のブロック図
【符号の説明】
【００９５】
１０１…デジタル回路検証装置、１０２…検証プログラム選択部、１０３…検証プログラム読取部、１０４…共有記憶部、１０５…検証プログラム解釈部、１０６…検証結果表示・記憶装置、１０７…変数実体判定部、１０８…変数読取部、１０９…変数書込部、１１０…アサーション付きハードウェア設計記述、１１１…ハードウェア設計記述、１１２…時相論理式、１１３…検証プログラム、１１４…ハードウェア設計記述シミュレータ、１１５…ハードウェア設計記述解釈部、１１６…テストベンチ、１１７…信号変化履歴、１１８…時相論理式判定部、１１９…信号記憶部、１２０…テストベンチ実行結果
【図１】
2008299629.tif 000003
【図２】
2008299629.tif 000004
【図３】
2008299629.tif 000005
【図４】
2008299629.tif 000006
【図５】
2008299629.tif 000007
【図６】
2008299629.tif 000008
【図７】
2008299629.tif 000009
【図８】
2008299629.tif 000010
【図９】
2008299629.tif 000011
【図１０】
2008299629.tif 000012
【図１１】
2008299629.tif 000013
【図１２】
2008299629.tif 000014
【図１３】
2008299629.tif 000015
【図１４】
2008299629.tif 000016
【図１５】
2008299629.tif 000017
【図１６】
2008299629.tif 000018
【図１７】
2008299629.tif 000019
【図１８】
2008299629.tif 000020