(57)【要約】【課題】  修正されたブロックの影響を、その出力条件が接続される非修正ブロックの入力条件を満たす箇所でのみ検証することで、短時間で正確に漏れなくハードウエア全体の動作を保証する手段を提供する。【解決手段】  修正ブロックの抽出手段と、抽出された修正ブロックからの出力条件が接続された非修正ブロックの抽出手段と、抽出された非修正ブロックの入力条件を修正前のハードウエア全体の制約条件から求める手段と、求められた制約条件を修正後のブロックからの入力条件が満たしていることを確認する手段、を具備する構成。【選択図】  図１
2007026176.tif 000002
【特許請求の範囲】
【請求項１】
複数の内部ブロックで構成されたハードウエアにおいて、
前記ハードウエア修正後の修正ブロックからの入力条件がある非修正ブロックを抽出する手段と、
前記ハードウエアの論理機能を検証する検証手段と、
前記抽出手段により抽出された非修正ブロックに対する入力制約条件を前記検証手段から生成する手段と、
前記抽出された非修正ブロックの入力制約条件生成手段を具備してハードウエアの検証を行う手段とを具備することを特徴とする検証手法。
【請求項２】
前記修正後ハードウエアにおける、修正ブロックか非修正ブロックかを判断する手段は、前記ハードウエアの修正前および修正後の内部ブロックが等価であるか比較することを特徴とする請求項１記載の検証手法。
【請求項３】
前記内部ブロックの等価性比較手段は、内部ブロック単位のソースコード比較もしくは、動作合成結果の等価性検証により行うことを特徴とする請求項２記載の検証手法。
【請求項４】
前記修正ブロックからの入力条件がある非修正ブロックを抽出する手段は、前記修正ブロックの出力条件をソースコードから検出し、出力条件が接続された内部ブロックが前記内部ブロックの等価性比較手段により修正されていないブロックの場合に抽出することを特徴とする請求項１、請求項２、あるいは請求項３記載の検証手法。
【請求項５】
前記ハードウエアの論理機能を検証する検証手段は、前記ハードウエアの入力制約条件に対する出力期待条件を論理式で記述しハードウエアの正規化論理表現との等価性を論理的に検証することを特徴とする請求項１、請求項２、請求項３、あるいは請求項４記載の検証手法。
【請求項６】
前記抽出された非修正ブロックの入力制約条件を前記検証手段から生成する手段は、修正前の前記ハードウエアにおいて、前記入力制約条件が入力された内部ブロックの出力全状態を次段ブロックの入力制約条件とすることで前記抽出された非修正ブロックの入力制約条件を生成することを特徴とする請求項１、請求項２、請求項３、請求項４、あるいは請求項５記載の検証手法。
【請求項７】
前記抽出された非修正ブロックの入力制約条件を具備してハードウエアの検証を行う手段は、前記ハードウエアの入力制約条件に対する出力状態を論理的に検証する論理シミュレーションもしくは論理的等価性を演算により検証する静的検証であることを特徴とする請求項１、請求項２、請求項３、請求項４、請求項５、あるいは請求項６記載の検証手法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、複数の内部ブロックで構成されたハードウエアにおいて、ハードウエアの検証を行う検証手法に関する。
【背景技術】
【０００２】
ＬＳＩを含む論理システムの規模は、年毎に増加している。それに伴い、論理システムの複雑度は指数関数的に上昇し、要求仕様を満たす機能を検証する困難度も増加している。一方、市場では信頼性の高い商品が求められており、不具合が生じた場合は回収費等を伴い、ブランド力の低下を招き、競合他社に対する競争力の低下は事業存続に対する支障を伴う。そのため、論理システム検証の信頼性の向上を図る必要が生じている。
【０００３】
従来より、開発効率を向上するためハードウエアの流用は行われてきた。不具合の修正や要求仕様の追加などにより、流用するハードウエアを部分的に修正することで、新規設計に要する負荷を軽減するとともに、動作実績による信頼性の向上や、検証資産の流用による検証効率の向上が図れるという利点が見込まれた。
【０００４】
たとえば流用するハードウエアの内部ブロックに調停回路が存在し、この調停回路が仕様と異なる動作であることが発見されたことで、このブロックのみ修正することでハードウエアを流用するケースを考える。req_a，req_b，req_c３つの要求信号が発行され続けた場合にreq_a→req_b→req_c→req_aの順に公平な優先度で調停を行った結果、１つの要求信号に対して許可信号を与えることでstate_A, state_B, state_C, state_Aに移行するラウンドロビン型の調停回路であることが仕様であったにもかかわらず、実際の動作がreq_cが発行された場合は最優先で許可信号を与えられてstate_Cに移行するプライオリティ型の調停回路であったとする。この場合、この調停回路ブロックのみラウンドロビン型調停回路に変更することで、ハードウエアを流用することが期待できる。
【０００５】
又、従来例としては、例えば特許文献１をあげることが出来る。
【特許文献１】特開平６−２６６７９１号公報
【発明の開示】
【発明が解決しようとする課題】
【０００６】
しかしながら修正したブロックの動作が変わることにより、正常動作していた非修正ブロックが影響を受け、ハードウエア全体としての動作不具合を招く場合がある。さらに、修正ブロックもしくは修正ブロック内部回路がライブラリとして意図せず他のブロックで使用されていた場合や、VHDLにおけるgeneric parameterのように拡張利用されていた場合などは、不具合の原因特定が困難である。
【０００７】
たとえば上記従来例の場合、調停回路が接続された非修正ブロックが調停回路の修正による動作変更により影響を受け動作不具合を生じる可能性がある。この調停回路に接続された非修正ブロックからの要求信号req_cは、常に調停回路の状態がstate_Ａの時に発行し、かつ状態がstate_Bに移行すると発行を中止するといった制約条件があった場合、修正前のreq_c最優先のプライオリティ型調停回路では許可信号があたえられるため正常に動作する。しかし修正したことによりラウンドロビン型に変更された調停回路では、調停回路の機能が正常であり、かつreq_cの要求信号が出力されているにもかかわらず許可信号が与えられず、state_Ｃの状態になり得ないという不具合が生ずる。
【０００８】
このような場合、修正したブロックの動作は正常でありかつ、修正されていない非修正ブロックの動作実績もあるにもかかわらず、ハードウエア全体での不具合となり、不具合箇所の特定が困難である。また、上記例における調停回路がライブラリ化されており、意図せず使用されていたことで非修正ブロックと思われていたブロックが修正されてしまった場合や、上記例における要求信号・許可信号の数がVHDLのgeneric parameterのように変更可能であった場合、すべてのケースでの動作保証および変更箇所の特定は極めて困難である。
【０００９】
本発明は、上記課題を解決するためになされたもので、修正されたブロックの影響を、その出力条件が接続される非修正ブロックの入力条件を満たす箇所でのみ検証することで、短時間で正確に漏れなくハードウエア全体の動作を保証する手段を提供する。
【課題を解決するための手段】
【００１０】
本出願に係わる第１の発明は、
修正ブロックの抽出手段と、抽出された修正ブロックからの出力条件が接続された非修正ブロックの抽出手段と、抽出された非修正ブロックの入力条件を修正前のハードウエア全体の制約条件から求める手段と、求められた制約条件を修正後のブロックからの入力条件が満たしていることを確認する手段、
を具備することを特徴とする。
【発明の効果】
【００１１】
以上説明したように、本発明によれば非修正ブロックが修正ブロックの影響を受けることによる動作不具合を確認できることにより、修正したブロックの動作は正常でありかつ、修正されていない非修正ブロックの動作実績もあるにもかかわらず、ハードウエア全体での不具合となり、不具合箇所の特定が困難な場合でも検証可能である。
【００１２】
また、修正ブロックがライブラリ化されており、意図せず使用されていたことで非修正ブロックと思われていたブロックが修正されてしまった場合や、上記例におけるVHDLのgeneric parameterのように変更可能なパラメータで使用されていることで意図されない拡張機能で使用され、すべてのケースでの動作保証および変更箇所の特定は極めて困難である場合で検証可能である。
【００１３】
その結果、本発明は、修正されたブロックの影響を、その出力条件が接続される非修正ブロックの入力条件を満たす箇所でのみ検証することで、短時間で正確に漏れなくハードウエア全体の動作を保証する手段を提供する。
【発明を実施するための最良の形態】
【００１４】
以下、図面を参照しながら本発明の実施形態を説明する。
【００１５】
図１は、本発明の一実施例を示す図である。
【００１６】
１０１は検証対象のハードウエア、１０２から１０５はハードウエア１０１の内部ブロックを示し、１０２は修正を行った修正ブロックであるところの調停回路、１０３から１０４は修正を行わなかった非修正ブロックであり、１０３は内部ブロック起動回路、１０４は調停回路１０２から許可信号を得られた場合にハードウエア１０１からの出力信号を生成するハードウエア出力信号生成回路、１０５は非修正回路１０４からの指示に同期してハードウエア１０１からの出力信号を生成するハードウエア同期出力信号生成回路を示す。１０６および１０７は修正ブロック１０２に接続される非修正ブロックの接続ポートを示し、１０６は修正ブロック１０２への出力条件であるところの調停回路１０２の起動信号、１０７は修正ブロック１０２との出力条件および入力条件であるところの調停信号を示す。１０８は修正ブロック１０２からの入力条件がある非修正ブロック１０４のすべての入力条件を示し、非修正ブロック１０３からの起動信号および調停回路１０２からの調停許可信号を示す。１０９および１１０は検証対象のハードウエア１０１の外部仕様条件を示し、１０９は内部ブロックの起動および調停回路１０２への外部入出力の仕様条件、１１０はハードウエアからの出力仕様条件を示す。
【００１７】
修正前のハードウエア１０１は、ハードウエア入出力条件１０９および１１０を満たしていたとする。このハードウエア１０１を修正した場合の、修正前のハードウエアと修正後のハードウエアを比較することで、修正箇所が存在する内部ブロックを抽出する手段について述べる。ハードウエア１０１がハードウエア記述言語VHDLで記述されている場合を例にとると、各内部ブロック１０２から１０５ごとにVHDLのソースコードおよびソースコード内で使用されているライブラリやパッケージを比較することで、各内部ブロックが修正されたかどうか判断することが可能となる。ソースコードに比較判断手段としてはUNIX（登録商標）コマンドにおけるdiffなどが使用できる。もしくは内部ブロックごとに動作合成を行い、修正前と修正後の動作等価性の比較を行う検証装置の利用も可能である。
【００１８】
次に修正ブロックからの出力条件が接続される非修正ブロックの抽出を行う。上記比較手段により抽出された修正ブロック１０２からの出力条件の接続先を抽出することで、非修正ブロック１０４のみが抽出される。ハードウエア１０１がハードウエア記述言語VHDLで記述されている場合を例にとると、ＶＨＤＬソースコードを走査することで、エンティティに記述されたoutputポートを抽出し、前記outputポートから出力される信号が接続されたＶＨＤＬソースコードを抽出することが可能である。
【００１９】
各内部ブロック１０２から１０５ごとにVHDLのソースコードおよびソースコード内で使用されているライブラリやパッケージを比較することで、各内部ブロックが修正されたかどうか判断することが可能となる。
【００２０】
そして修正前のハードウエア１０１において、ハードウエア外部仕様条件１０９および１１０から、抽出された非検証ブロックであるハードウエア出力信号生成回路１０４に入力されるすべての入力条件１０８を作成する。ここではVHDLなどの論理回路記述および論理関数をBDD(Binary Decision Diagram)、真理値表、積和標準形などの表現方法に変換し、入力条件に対する出力条件を定める手法を用いることができる。真理値表は入力数の指数乗の項数を必要とする。また、積和標準形も最悪の場合、真理値表と同じく入力数の指数乗の項数を必要とする。しかし、BDDでは多くの場合、真理値表や積和標準形より少ない項数で論理関数を表現可能である。また、真理値表と積和標準形では、内部表現への変換工数が論理関数の複雑度に影響し、複雑になるにつれて内部表現への変換工数が増加する。一方、BDDでは論理関数の複雑度に関係なく変換工数がきまる。そのこで、本実施例では、内部表現としてBDDを用いることとする。勿論、内部表現をBDDに限定するのもではなく、同一の論理関数が同一の表現になるならばどのような表現を用いてよい。
【００２１】
VHDLなどの論理回路記述をBDDに変換する手法としてはapplyアルゴリズムを使用することができる。このapplyアルゴリズムは 1984にRandal E. Bryant氏により開発された、BDD生成アルゴリズムである。このapplyアルゴリズムは、既に数多く使用されており、公知の技術である。
【００２２】
論理関数表現例の書式を以下に示す。
;       動作記述の区切り
a=>b    aが成立するならばbが成り立つ
&&      論理積
||      論理和
~      論理否定
'      次クロック・サイクルの状態
'(n)   nクロック・サイクルの状態
//     コメント
ここでハードウエア１０１の外部仕様条件による内部ブロック起動回路１０３へのリセット信号はreset、前記reset解除時に内部ブロック起動回路１０３から調停回路１０２とハードウエア出力条件生成回路１０４を起動する出力信号を、それぞれarb_enableとoutput_enableとする。ハードウエア１０１の外部仕様条件による調停回路１０２への２入力の要求信号はそれぞれreq_aおよびreq_b、ハードウエア出力信号生成回路１０４からの出力される要求信号はreq_cとする。req_bはハードウエア出力信号生成回路１０４にも入力されているとする。また、調停回路１０２からハードウエア出力信号生成回路１０４に対し出力されるところの許可信号はstate_Cとする。
【００２３】
まずハードウエア外部仕様条件１０９により、内部ブロックの起動回路１０３に入力されたリセット信号resetが解除されると、次のサイクルで起動回路１０３は調停回路１０２およびハードウエア出力信号生成回路１０４を起動する仕様であった場合、resetの入力条件から
(~reset)=>`(arb_enable);  --  1001
(~reset)=>`(output_enable);  --  1002
が求められる。そしてこのoutpur_enableが発行され、かつreq_a要求信号に対する許可信号であるところのstate_Aが発行されていることより、ハードウエア出力信号生成回路１０４からの要求信号req_cが発行される仕様であった場合、
(output_enable  &&  state_A)=>(req_c);  --  1003
が求められる。そして調停回路１０２からの許可信号state_Cの出力条件は、arb_enableが発行されている状態でかつ、req_c要求信号が発行されると、req_aもしくはreq_b要求信号の状態に関わらず、次のサイクルで最優先にstate_C許可信号を発行するプライオリティ型の調停回路であった場合、
(arb_enable && req_c)=>`(state_C);  --  1004
が求められる。ここで1003式を1004式に埋め込むことにより、
(arb_enable && output_enable && state_A)=>`(state_C);  --  1005
さらに1001式と1002式からarb_enableはoutput_enableと同等条件のため最適化することで、
(output_enable && state_A)=>`(state_C);  --  1006
が導き出される。つまり、ハードウエア出力信号生成回路１０２のすべての入力信号における入力条件１０８として、output_enableおよびstate_Aが発行された次のサイクルで、state_C許可信号が入力されるということが求められる。
【００２４】
以上の方法で求められたハードウエア出力条件生成回路１０４の入力条件１０８を、修正後のハードウエア１０１の外部動作仕様１０９・１１０が満たすかを確認することで、修正ブロックが変更されたことによる、非修正ブロックの動作不具合を検出することが可能となる。これを、調停回路１０２が修正された場合の実施例で示す。
【００２５】
修正前の調停回路１０２は前述したように、req_c要求信号が入力されると最優先にstate_C許可信号を発行するプライオリティ型の調停回路であったが、req_a，req_b，req_c３つの要求信号が発行され続けた場合にreq_a→req_b→req_c→req_aの順に公平な優先度で調停を行った結果、１つの要求信号に対して許可信号を与えるラウンドロビン型の調停回路に変更した例を示す。
【００２６】
図２はラウンドロビン型調停回路をＢＤＤ解析した結果の２分決定グラフを最適化したものであり、次のサイクルでreq_cに対する許可信号であるところのstate_Cが発行される条件を示している。２分決定グラフはすべて、右枝が論理‘１’左枝が‘０’であるとする。たとえば上から順に、arb_enableが‘１’で、req_cが‘１’で、req_aが‘１’で、req_bが‘０’の場合、右枝→右枝→右枝→左枝となるため、state_A許可信号を出力しているかの条件判断となる。ここでstate_Aにいた場合、右枝となるためstate_C許可信号は‘１’となって出力されることとなる。これはラウンドロビン型の公平な優先度の調停回路の場合は、state_A許可信号を受け取っているreq_aが発行されていたとしても、req_cが発行された場合はstate_Cに許可信号を切り替えることを示している。一方state_Aにいなかった場合、左枝となるためstate_B許可信号を出力しているかの条件判断となるわけだが、まずstate_Bにいた場合、req_aとreq_cの要求信号が発行されると次はラウンドロビンの順番からstate_Cが優先となるため、右枝の‘１’となりstate_C許可信号が発行されることとなる。一方、state_Bにいなかった場合、すでにstate_Aではなかったことからstate_Cにいたことが自明であるため、req_cが発行されていたとしても、req_aが発行された場合はstate_C許可信号を停止してstate_Aに切り替えることを示している。
【００２７】
図３は図２のＢＤＤ２分決定グラフより、修正後のラウンドロビン型調停回路の入力条件に対する出力条件を検出した結果の例である。state_C許可信号を発行する条件としては、
(arb_enable && state_A             && ~req_b &&  req_c) => '(state_C);
-- 1007
(arb_enable && state_B                         &&  req_c) => '(state_C);
-- 1008
(arb_enable && state_C && ~req_a && ~req_b &&  req_c) => '(state_C); 
-- 1009
(arb_enable && state_A || state_B || state_C) =>
'(state_A) || '(state_B) || '(state_C);                      -- 1010
があげられる。ここでたとえば式1005に式1001,1002,1003を適用して最適化すると、
(state_A             && ~req_b &&  output_enable) =>  '(state_C);
-- 1011
が導き出される。つまり、output_enableおよびstate_Aがハードウエア出力信号生成回路１０４に発行されることにより、調停回路に対してreq_cが発行されたとしても、req_bが発行されている場合は、次のサイクルでstate_Cに移行することはない。
【００２８】
以上のことから、修正前のハードウエア１０１において、ハードウエア出力信号生成回路１０４の入力条件１０８を求めた式であるところの、
(output_enable && state_A)=>`(state_C);                        --  1006
を、調停回路１０２をラウンドロビン型に修正した後のハードウエアにおいて検証した場合、1011式、
(state_A             && ~req_b &&  output_enable) =>  '(state_C);
-- 1011
が前記1006式を満たさないため、非修正ブロックであるところのハードウエア出力信号生成回路１０４が期待する入力条件を、修正ブロックであるラウンドロビン型調停回路１０２が満たしていないため、動作不具合を生じる可能性があることがわかる。
【００２９】
つまり、式1003で説明したように、ハードウエア出力信号生成回路１０４からの要求信号req_cは、調停回路の状態がstate_Ａであり、かつ状態がstate_Bに移行すると発行を中止するといった制約条件があるため、修正前のreq_c最優先のプライオリティ型調停回路ではstate_C許可信号があたえられ正常に動作していたにもかかわらず、ラウンドロビン型に変更された調停回路では、調停回路の機能が正常であり、かつreq_cの要求信号が出力されているにもかかわらずstate_C許可信号が与えられないという不具合が生ずる。
【００３０】
よって、修正前のハードウエア１０１の外部動作仕様１０９・１１０により生成したハードウエア出力条件生成回路１０４の入力条件１０８を、修正後のハードウエア１０１の外部動作仕様１０９・１１０が満たすかを確認することで、修正ブロックが変更されたことによる影響により非修正ブロックが動作不具合を起こさないか検出することが可能となる。
【００３１】
図４は以上述べた本発明のアルゴリズムを示している。
【００３２】
Ｓ００１は、修正前と修正後のハードウエアを比較し、修正ブロックの抽出を示す。
【００３３】
Ｓ００２は、修正ブロックの出力条件が接続された非修正ブロックの抽出を示す。
【００３４】
Ｓ００３は、修正前のハードウエアの入出力条件を満たす、前記非修正ブロックの入力条件の検出を示す。
【００３５】
Ｓ００４は、修正後のハードウエアに入出力条件をあたえ、前記非修正ブロックの入力条件を満たしているか確認することを示す。
【００３６】
Ｓ００５は、前記非修正ブロック入力条件を満たしているかの判断・検証を示す。
【００３７】
Ｓ００６は、Ｓ００５で前記非修正ブロック入力条件を満たしていない場合、非修正ブロックに出力条件のある修正ブロックの仕様を確認することを示す。
【００３８】
Ｓ００７は、修正ブロックの再修正、もしくは非修正ブロックを修正することを示す。
【００３９】
以上述べた発明の実施例において、修正前のハードウエア１０１の外部動作仕様１０９・１１０により生成したハードウエア出力条件生成回路１０４の入力条件１０８を、修正後のハードウエア１０１が満たすかの確認に用いるハードウエア外部動作仕様１０９・１１０は修正前のハードウエアの外部動作仕様に限定されるものではない。新たに期待されるハードウエア外部動作仕様を、修正後のハードウエアが満たしているか判断することで、追加仕様に適合したうえで、非修正ブロックが修正ブロックの影響を受けてないことの確認も可能である。
【００４０】
また、修正前のハードウエア１０１の外部動作仕様１０９・１１０により生成したハードウエア出力条件生成回路１０４の入力条件１０８の生成は、入力の外部動作仕様から生成されるものに限定されるものではない。出力の外部動作仕様を満たす内部ブロックの入力条件を順次求める手法も同様に適用可能である。
【００４１】
また、修正前のハードウエア１０１の外部動作仕様１０９・１１０および、外部動作仕様より生成したハードウエア出力条件生成回路１０４の入力条件１０８は、論理式による条件式に限るものではない。ハードウエア出力条件生成回路の入力条件を監視するアサーション記述もしくはチェッカーとして、外部動作仕様を動的シミュレーションによる入力とし検証を行うことでも同様の効果が得られる。
【図面の簡単な説明】
【００４２】
【図１】本発明の一実施例を示す図。
【図２】ラウンドロビン型調停回路をＢＤＤ解析した結果の最適化２分決定グラフ。
【図３】ラウンドロビン型調停回路の入力条件に対する出力条件を検出した結果例。
【図４】本発明のアルゴリズム。
【符号の説明】
【００４３】
１０１  検証対象のハードウエア
１０２  修正を行った修正ブロックであるところの調停回路
１０３  非修正ブロックであるところの内部ブロック起動回路
１０４  非修正ブロックであるところのハードウエア出力信号生成回路
１０５  非修正ブロックであるところのハードウエア同期出力信号生成回路
１０６  修正ブロック１０２への出力条件であるところの調停回路１０２の起動信号
１０７  修正ブロック１０２との出力条件および入力条件であるところの調停信号
１０８  非修正ブロック１０４のすべての入力条件
１０９  内部ブロックの起動および調停回路１０２への外部入出力の仕様条件
１１０  ハードウエアからの出力仕様条件
【図１】
2007026176.tif 000003
【図２】
2007026176.tif 000004
【図３】
2007026176.tif 000005
【図４】
2007026176.tif 000006