図面 (/)

技術 検証装置、検証方法及びプログラム

出願人 富士通セミコンダクター株式会社
発明者 星川大輔
出願日 2011年8月10日 (8年7ヶ月経過) 出願番号 2011-174675
公開日 2013年2月21日 (7年0ヶ月経過) 公開番号 2013-037607
状態 未査定
技術分野 CAD 半導体集積回路 ICの設計・製造(配線設計等)
主要キーワード 実使用レベル 検証コスト 形式検証 検証対象データ 光学ドライブ装置 検証用情報 動作レベル 形式的検証
関連する未来課題
重要な関連分野

この項目の情報は公開日時点(2013年2月21日)のものです。
また、この項目は機械的に抽出しているため、正しく解析できていない場合があります

図面 (12)

課題

検証する範囲を少なくして、検証コストや検証時間の増大を抑制する。

解決手段

抽出部12が、第1のクロック信号で動作する回路部21と、第2のクロック信号で動作する回路部22とを含む検証対象回路論理回路20)から、ハンドシェイクの手順に従って回路部21と回路部22間でのデータの送受信を行うハンドシェイク部23を抽出し、検証部13が抽出されたハンドシェイク部23の信号が、その手順を満たすかを検証し、手順を満たさない信号があるとき、回路部21と回路部22のうち当該信号を出力する側で、当該信号が手順を満たさなくなる条件が回路動作時に起こり得るか検証する。

概要

背景

異なるクロック信号で動作する回路部間で、複数ビットの信号のやり取りを行う際、ハンドシェイクと呼ばれる手順が行われる。
第1のクロック信号で動作する回路部(以下Aクロックドメインと呼ぶ)のデータ(A_DATA)を、第2のクロック信号で動作する回路部(以下Bクロックドメインと呼ぶ)に渡す場合、たとえば、以下のようなハンドシェイクの手順が行われる。

まず、Aクロックドメイン側で、データを送信するためのリクエスト信号(A_REQ)がアサートされる。次に、Bクロックドメインのフリップフロップ(以下FFと略す)を2回介したA_REQであるA_REQ_q2がアサートされる。A_REQ_q2がアサートされると、Bクロックドメイン側がA_DATAをB_DATAとして受信する。

その後、Bクロックドメイン側で、受信が行われたことを示す信号(B_ACK)がアサートされる。次に、AクロックドメインのFFを2回介したB_ACKであるB_ACK_q2がアサートされる。続いて、Aクロックドメイン側で、A_REQがデアサートされる。そして、BクロックドメインのFFを2回介したA_REQであるA_REQ_q2がデアサートされる。

その後、Bクロックドメイン側で、B_ACKがデアサートされ、AクロックドメインのFFを2回介したB_ACKであるB_ACK_q2がデアサートされる。
このような手順の際に、たとえば、Bクロックドメインで、B_ACKをアサートすべきときに、Bクロックドメインだけのリセットや、ある条件などによりB_ACKがアサートされなくなった場合、AクロックドメインはB_ACK_q2がアサートされることを待ち続けることになり、デッドロックが発生する可能性がある。

一方、非同期検証を行う手法としては、従来、回路全体に対する動的検証が行われていた。たとえば、上記のようなハンドシェイクを行う部分では、各クロック線あるいは信号線に対して任意のジッター値ランダムに与えられ、動的検証が実施され、その結果から回路の妥当性が確認されていた。

概要

検証する範囲を少なくして、検証コストや検証時間の増大を抑制する。抽出部12が、第1のクロック信号で動作する回路部21と、第2のクロック信号で動作する回路部22とを含む検証対象回路論理回路20)から、ハンドシェイクの手順に従って回路部21と回路部22間でのデータの送受信を行うハンドシェイク部23を抽出し、検証部13が抽出されたハンドシェイク部23の信号が、その手順を満たすかを検証し、手順を満たさない信号があるとき、回路部21と回路部22のうち当該信号を出力する側で、当該信号が手順を満たさなくなる条件が回路動作時に起こり得るか検証する。

目的

効果

実績

技術文献被引用数
0件
牽制数
0件

この技術が所属する分野

ライセンス契約や譲渡などの可能性がある特許掲載中! 開放特許随時追加・更新中 詳しくはこちら

請求項1

第1のクロック信号で動作する第1の回路部と、第2のクロック信号で動作する第2の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第1の回路部と前記第2の回路部間でのデータの送受信を行うハンドシェイク部を抽出する抽出部と、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する検証部と、を有することを特徴とする検証装置

請求項2

前記信号が、前記データの送受信時に満たすべき条件を記述した第1の検証用情報を生成する検証用情報生成部を有し、前記検証部は、生成された前記第1の検証用情報を用いて、前記信号が前記手順を満たすか否か検証することを特徴とする請求項1に記載の検証装置。

請求項3

前記検証用情報生成部は、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記データの送受信時に前記手順を満たす場合の条件を記述した第2の検証用情報を生成し、前記検証部は、生成された前記第2の検証用情報を用いて、前記信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証することを特徴とする請求項2に記載の検証装置。

請求項4

コンピュータによって実行される検証方法であって、第1のクロック信号で動作する第1の回路部と、第2のクロック信号で動作する第2の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第1の回路部と前記第2の回路部間でのデータの送受信を行うハンドシェイク部を抽出し、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する、ことを特徴とする検証方法。

請求項5

第1のクロック信号で動作する第1の回路部と、第2のクロック信号で動作する第2の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第1の回路部と前記第2の回路部間でのデータの送受信を行うハンドシェイク部を抽出し、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する、処理をコンピュータに実行させるプログラム

技術分野

0001

本発明は、検証装置検証方法及びプログラムに関する。

背景技術

0002

異なるクロック信号で動作する回路部間で、複数ビットの信号のやり取りを行う際、ハンドシェイクと呼ばれる手順が行われる。
第1のクロック信号で動作する回路部(以下Aクロックドメインと呼ぶ)のデータ(A_DATA)を、第2のクロック信号で動作する回路部(以下Bクロックドメインと呼ぶ)に渡す場合、たとえば、以下のようなハンドシェイクの手順が行われる。

0003

まず、Aクロックドメイン側で、データを送信するためのリクエスト信号(A_REQ)がアサートされる。次に、Bクロックドメインのフリップフロップ(以下FFと略す)を2回介したA_REQであるA_REQ_q2がアサートされる。A_REQ_q2がアサートされると、Bクロックドメイン側がA_DATAをB_DATAとして受信する。

0004

その後、Bクロックドメイン側で、受信が行われたことを示す信号(B_ACK)がアサートされる。次に、AクロックドメインのFFを2回介したB_ACKであるB_ACK_q2がアサートされる。続いて、Aクロックドメイン側で、A_REQがデアサートされる。そして、BクロックドメインのFFを2回介したA_REQであるA_REQ_q2がデアサートされる。

0005

その後、Bクロックドメイン側で、B_ACKがデアサートされ、AクロックドメインのFFを2回介したB_ACKであるB_ACK_q2がデアサートされる。
このような手順の際に、たとえば、Bクロックドメインで、B_ACKをアサートすべきときに、Bクロックドメインだけのリセットや、ある条件などによりB_ACKがアサートされなくなった場合、AクロックドメインはB_ACK_q2がアサートされることを待ち続けることになり、デッドロックが発生する可能性がある。

0006

一方、非同期検証を行う手法としては、従来、回路全体に対する動的検証が行われていた。たとえば、上記のようなハンドシェイクを行う部分では、各クロック線あるいは信号線に対して任意のジッター値ランダムに与えられ、動的検証が実施され、その結果から回路の妥当性が確認されていた。

先行技術

0007

特開2006−252438号公報
特開2011−34475号公報

発明が解決しようとする課題

0008

しかしながら、従来の手法では、回路全体に対して検証を行うことになるため、ハンドシェイクを行う部分以外の機能検証も同時に行うことになる。そのため、検証を実施する条件の組み合わせが膨大なものになり、検証コストや、検証時間が増加する問題があった。

課題を解決するための手段

0009

発明の一観点によれば、以下に示すような検証装置が提供される。
この検証装置は、第1のクロック信号で動作する第1の回路部と、第2のクロック信号で動作する第2の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第1の回路部と前記第2の回路部間でのデータの送受信を行うハンドシェイク部を抽出する抽出部と、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する検証部と、を備える。

発明の効果

0010

開示の検証装置、検証方法及びプログラムによれば、検証する範囲を少なくでき、検証コストや検証時間の増大を抑制することができる。

図面の簡単な説明

0011

第1の実施の形態の検証装置の一例を示す図である。
ハンドシェイクの手順の一例を示す図である。
ハンドシェイク部のRTL(Register Transfer Level)の回路記述一つ目の例である。
ハンドシェイク部のRTLの回路記述の二つ目の例である。
第2の実施の形態の検証装置の一例を示す図である。
第2の実施の形態の検証装置による検証方法の一例の流れを説明するフローチャートである。
検証プロパティAの例を示す図である。
検証プロパティ名が1_b_ack_astの検証プロパティAを用いた検証でエラーが発生したときに生成される検証プロパティBの例である。
検証プロパティ名が2_a_req_dastの検証プロパティAを用いた検証でエラーが発生したときに生成される検証プロパティBの例である。
検証プロパティ名が3_b_ack_dastの検証プロパティAを用いた検証でエラーが発生したときに生成される検証プロパティBの例である。
本実施の形態に用いるコンピュータハードウェアの一構成例を示す図である。

実施例

0012

以下、本発明の実施の形態を、図面を参照しつつ説明する。
(第1の実施の形態)
図1は、第1の実施の形態の検証装置の一例を示す図である。

0013

検証装置10は、記憶部11、抽出部12、検証部13を有している。
記憶部11は、検証対象データD1を記憶している。検証対象データD1は、検証対象回路(図1の例では論理回路20)を、たとえば、Verilogや、VHDL(Very high speed integrated circuit Hardware Description Language)などのハードウェア記述言語などで記述したデータである。

0014

論理回路20は、互いに異なるクロックで動作する回路部21,22を有するものである。すなわち、回路部21,22は、異なるクロックで動作するクロックドメインとなる。

0015

回路部21,22間でハンドシェイクの手順に従ってデータの送受信を行う部分が、ハンドシェイク部23である。ハンドシェイク部23には、複数のFFが含まれる。
抽出部12は、論理回路20から、ハンドシェイク部23を抽出する。たとえば、抽出部12は、検証対象データD1に含まれる論理回路20の回路記述から、ハンドシェイク部23の回路記述を抽出する。

0016

検証部13は、抽出されたハンドシェイク部23に対して、シミュレーションを行い、ハンドシェイク部23の信号が、ハンドシェイクの手順を満たすか検証する。ハンドシェイクの手順を満たさない信号があるとき、検証部13は、回路部21,22のうち、その信号を出力する側で、その信号がハンドシェイクの手順を満たさなくなる条件が、回路動作時に起こり得るか検証する。

0017

図2は、ハンドシェイクの手順の一例を示す図である。
図2では、回路部21がA_DATA[*:0]というデータを回路部22に送信するときのハンドシェイクの手順の一例が示されている。FF30,31は、ハンドシェイク部23の回路部22側に含まれるFFであり、回路部22で用いられるクロック信号がクロック端子に入力される。FF32,33は、ハンドシェイク部23の回路部21側に含まれるFFであり、回路部21で用いられるクロック信号がクロック端子に入力される。

0018

回路部21がA_DATA[*:0]というデータを回路部22に送信するとき、回路部22は、リクエスト信号(A_REQ)をアサートする(図2の例では“1”とすることを示す)。

0019

A_REQは、回路部22のFF30に入力される。回路部22で用いられるクロック信号に同期して、A_REQはFF30からFF31に伝達され、FF31の出力信号であるA_REQ_q2がアサートされる。A_REQ_q2がアサートされると、回路部22側で、A_DATAがB_DATAとして受信される。

0020

その後、回路部22側で、受信が行われたことを示す信号(B_ACK)がアサートされる。B_ACKは、回路部21のFF32に入力される。回路部21で用いられるクロック信号に同期して、B_ACKはFF32からFF33に伝達され、FF33の出力信号であるB_ACK_q2がアサートされる。

0021

B_ACK_q2がアサートされると、回路部21は、A_REQをデアサートする(図2の例では“0”とすることを示す)。
A_REQの変化は、回路部22のFF30,31を介して伝わり、A_REQ_q2がデアサートされる。

0022

A_REQ_q2がデアサートされると、回路部22は、B_ACKをデアサートする。
B_ACKの変化は、回路部21のFF32,33を介して伝わり、B_ACK_q2がデアサートされる。

0023

図3は、ハンドシェイク部のRTL(Register Transfer Level)の回路記述の一つ目の例である。回路記述は、Verilogで記述されており、前述したハンドシェイク部23の回路部22側で出力される信号であるB_ACKが変化する条件が示されている。

0024

図3の1行目では、回路部22のクロック信号(BCLK)の立ち上がりエッジ、または、論理回路20のリセット信号(RST)の立ち下がりエッジに同期して、以下の行の処理を行うことが示されている。2,3行目では、RSTが0のとき、B_ACKが0(B_ACK<=1’b0)となることが示されている。なお、1’は1ビットを示し、bは2進数であることを示している。

0025

4,5行目では、RSTが0でないとき、回路部22のみのリセット信号(B_RST)が0、回路部22内のカウンタ値(B_CNT)が15のとき、もしくはA_REQ_q2が0で、かつB_CNTが0のとき、B_ACKが0となることが示されている。なお、4’は4ビット、hは16進数であることを示している。

0026

6,7行目では、A_REQ_q2が1のときに、B_ACKが1となることが示されている。
図4は、ハンドシェイク部のRTLの回路記述の二つ目の例である。回路記述は、Verilogで記述されており、前述したハンドシェイク部23の回路部21側で出力される信号であるA_REQが変化する条件が示されている。

0027

図4の1行目では、回路部21のクロック信号(ACLK)の立ち上がりエッジ、または、論理回路20のリセット信号(RST)の立ち下がりエッジに同期して、以下の行の処理を行うことが示されている。2,3行目では、RSTが0のとき、A_REQが0となることが示されている。4,5行目では、RSTが0でないとき、回路部21内のカウンタ値(A_CNT)が2、かつB_ACK_q2が1のとき、A_REQが0となることが示されている。6,7行目では、A_CNTが0のときに、A_REQが1となることが示されている。

0028

検証部13は、抽出された、図3図4のようなハンドシェイク部23の回路記述において、A_REQやB_ACKなどの信号が、図2に示したようなハンドシェイクの手順を満たすか検証する。

0029

たとえば、検証部13は、A_REQ_q2がアサートされたにもかかわらず、回路部22だけのリセットや、ある条件などによりB_ACKがアサートされなくなった場合、B_ACKがハンドシェイクの手順を満たさないと判定する。

0030

このとき、検証部13は、B_ACKを出力する側の回路部22で、B_ACKがアサートされない条件が、回路動作時に起こり得るか検証する。
このように、本実施の形態の検証装置10によれば、ハンドシェイク部23の検証を行い、ハンドシェイクの手順を満たさない信号があるときには、その信号を出力する側の回路部で検証を行うので、検証する範囲を少なくできる。これにより、検証コストや検証時間の増大を抑制することができる。

0031

(第2の実施の形態)
図5は、第2の実施の形態の検証装置の一例を示す図である。
第1の実施の形態の検証装置10と同様の要素については同一符号を付し、説明を省略する。

0032

第2の実施の形態の検証装置10aは、検証用情報生成部14を有している。検証用情報生成部14は、抽出部12で抽出されたハンドシェイク部23の信号をもとに、検証部13で検証を行うための検証用情報(以下検証プロパティと呼ぶ)を生成する。

0033

検証用情報生成部14は、検証部13が行う2段階の検証、すなわち、前述したハンドシェイク部23の検証と、ハンドシェイクの手順を満たさないと判定された信号を出力する側の回路部の検証の、それぞれの検証用の検証プロパティを生成する。検証プロパティは、たとえば、System Verilog、e言語、PSL(Property Specification Language)などの検証記述言語で記述される。

0034

ハンドシェイク部23の検証用に生成される検証プロパティには、データ送受信時に、ハンドシェイク部23の信号が満たすべき条件(つまりハンドシェイクの手順を満たすような条件)が記述される。

0035

ハンドシェイクの手順を満たさないと判定された信号を出力する側の回路部の検証時に生成される検証プロパティには、手順を満たさないと判定された信号が、その回路部において、データ送受信時に手順を満たす場合の条件が記述される。

0036

そして、検証部13は、この2種類の検証プロパティを用いて検証を行う。2番目の検証では、検証部13は、検証プロパティBに記述された条件がになる場合が、回路動作時において存在するか否かによって、回路部21,22間のデータ送受信時にデッドロックが発生するか否か検証する。

0037

図6は、第2の実施の形態の検証装置による検証方法の一例の流れを説明するフローチャートである。
なお、以下では、図1に示したような論理回路20に対して検証を行う場合を例にして説明する。

0038

まず、抽出部12は、論理回路20から、ハンドシェイク部23を抽出する(ステップS10)。たとえば、抽出部12は、論理回路20の回路記述から、図3図4に示したようなハンドシェイク部23の回路記述を抽出する。

0039

さらに、抽出部12は、ハンドシェイク部23の信号(A_REQ,A_REQ_q2,B_ACK,BACK_q2)を抽出する(ステップS11)。
ステップS10,S11の処理において、抽出部12は、0−In CDC(Clock Domain Crossing)などの検証ツールを適用してもよい。

0040

その後、検証用情報生成部14は、抽出されたハンドシェイク部23とその信号をもとに、ハンドシェイク部23の検証を行うための検証プロパティ(以下検証プロパティAと呼ぶ)を生成する(ステップS12)。

0041

図7は、検証プロパティAの例を示す図である。
図7では、検証プロパティAとして、アサーション設計対象の論理回路で期待されている動作などを記述した文)をSystem Verilogで記述した、3つの検証プロパティの例が示されている。

0042

各検証プロパティの1行目の1_b_ack_ast、2_a_req_dast、3_b_ack_dastが、それぞれの検証プロパティ名である。
検証プロパティ名が1_b_ack_astの検証プロパティは、前述したハンドシェイクの手順のように、A_REQ_q2がアサートされるとB_ACKがアサートされるかどうかを検証するためのものである。

0043

2行目には、この検証プロパティの内容が記述されている。回路部22のクロック信号(BCLK)の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティを無効にすること、A_REQ_q2が1(アサート)の状態が1サイクル以上連続して成り立つ場合、次のサイクルでB_ACKが1(アサート)になることが示されている。

0044

3行目では、検証プロパティの終わりが示されており、4行目では、1_b_ack_astの検証プロパティが偽と判断された場合、エラーとすることが示されている。
検証プロパティ名が2_a_req_dastの検証プロパティは、前述したハンドシェイクの手順のように、B_ACK_q2がアサートされるとA_REQがデアサートされるかどうかを検証するためのものである。

0045

2行目には、この検証プロパティの内容として、回路部21のクロック信号(ACLK)の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティを無効にすること、B_ACK_q2が1(アサート)の状態が1サイクル以上連続して成り立つ場合、次のサイクルでA_REQが0(デアサート)になることが示されている。

0046

3行目では、検証プロパティの終わりが示されており、4行目では、2_a_req_dastの検証プロパティが偽と判断された場合、エラーとすることが示されている。
検証プロパティ名が3_b_ack_dastの検証プロパティは、前述したハンドシェイクの手順のように、A_REQ_q2がデアサートされるとB_ACKがデアサートされるかどうかを検証するためのものである。

0047

2行目には、この検証プロパティの内容として、回路部22のクロック信号(BCLK)の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティを無効にすること、A_REQ_q2が1(アサート)の状態が1サイクル以上連続して成り立つ場合、次のサイクルでB_ACKが0(デアサート)になることが示されている。

0048

3行目では、検証プロパティの終わりが示されており、4行目では、3_b_ack_dastの検証プロパティが偽と判断された場合、エラーとすることが示されている。
検証部13は、上記のような検証プロパティAを用いてハンドシェイク部23の形式的検証を行い(ステップS13)、エラーが発生するか否かを判定する(ステップS14)。

0049

図7に示した、検証プロパティ名が1_b_ack_astの検証プロパティAを適用した形式検証では、A_REQ_q2がアサートされるとB_ACKがアサートされるかどうかが検証される。たとえば、図3に示したように記述されているハンドシェイク部23の場合、回路部22のリセット信号(B_RST)が0になっていたりすると、A_REQ_q2がアサートの状態にもかかわらず、B_ACKは0となり、アサートされない。このような場合、検証部13はエラーが発生したと判定する。

0050

検証部13は、同様に、検証プロパティ名が2_a_req_dast,3_b_ack_dastの検証プロパティAについても検証を行い、エラーが発生するか否かを判定する。

0051

検証の結果、エラーが生じたと判定された場合、検証用情報生成部14は、ハンドシェイクの手順を満たさない信号を出力する側の回路部を検証するための検証プロパティ(以下検証プロパティBと呼ぶ)を生成する(ステップS15)。

0052

検証用情報生成部14は、たとえば、検証プロパティ名が1_b_ack_astの検証プロパティAを用いた検証でエラーが発生したときには、ハンドシェイク部23からB_ACK部分の論理トレースし、B_ACKが1にならない条件を抽出する。そして、検証用情報生成部14は、抽出した条件が、回路部22の動作レベルで発生するかどうかを確認する検証プロパティBを生成する。

0053

図8は、検証プロパティ名が1_b_ack_astの検証プロパティAを用いた検証でエラーが発生したときに生成される検証プロパティBの例である。
図8では、検証プロパティBとして、アサーションをSystem Verilogで記述した、2つの検証プロパティの例が示されている。

0054

各検証プロパティの1行目の4_b_ack_ast_practice,5_b_ack_ast_practice2が、それぞれの検証プロパティ名である。
検証プロパティ名が4_b_ack_ast_practiceの検証プロパティBでは、回路部22のクロック信号(BCLK)の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティBを無効にすること、A_REQ_q2が1(アサート)の状態が1サイクル以上連続したとき、B_RSTが1になっていることが示されている。

0055

検証プロパティ名が5_b_ack_ast_practice2の検証プロパティBでも、回路部22のクロック信号(BCLK)の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティBを無効にすること、A_REQ_q2が1(アサート)の状態が1サイクル以上連続したときには、回路部22のカウンタ値(B_CNT)は15ではないことが示されている。

0056

3行目では、検証プロパティBの終わりが示されており、4行目では、上記の検証プロパティBの内容が偽と判断された場合、エラーとすることが示されている。
検証用情報生成部14は、たとえば、検証プロパティ名が2_a_req_dastの検証プロパティAを用いた検証でエラーが発生したときには、ハンドシェイク部23からA_REQ部分の論理をトレースし、A_REQが0にならない条件を抽出する。そして、検証用情報生成部14は、抽出した条件が、回路の動作レベルで発生するかどうかを確認する検証プロパティBを生成する。

0057

図9は、検証プロパティ名が2_a_req_dastの検証プロパティAを用いた検証でエラーが発生したときに生成される検証プロパティBの例である。
1行目の6_a_req_ast_practiceが、検証プロパティ名である。

0058

2行目には、この検証プロパティBの内容が記述されており、回路部21のクロック信号(ACLK)の立ち上がりエッジに同期してこの検証プロパティBが動作することが示されている。さらに、RSTが0のとき、この検証プロパティBを無効にすること、B_ACK_q2が1(アサート)の状態が1サイクル以上連続するとき、次のサイクルでA_CNTが2になることが示されている。

0059

3行目では、検証プロパティBの終わりが示されており、4行目では、上記の検証プロパティBの内容が偽と判断された場合、エラーとすることが示されている。
検証用情報生成部14は、たとえば、検証プロパティ名が3_b_ack_dastの検証プロパティAを用いた検証でエラーが発生したときには、ハンドシェイク部23からB_ACK部分の論理をトレースし、B_ACKが1にならない条件を抽出する。そして、検証用情報生成部14は、抽出した条件が、回路の動作レベルで発生するかどうかを確認する検証プロパティBを生成する。

0060

図10は、検証プロパティ名が3_b_ack_dastの検証プロパティAを用いた検証でエラーが発生したときに生成される検証プロパティBの例である。
1行目の7_b_ack_ast_practiceが、検証プロパティ名である。

0061

2行目には、この検証プロパティBの内容が記述されており、回路部22のクロック信号(BCLK)の立ち上がりエッジに同期してこの検証プロパティBが動作することが示されている。さらに、RSTが0のとき、この検証プロパティBを無効にすること、A_REQ_q2が1(アサート)の状態が1サイクル以上連続するとき、次のサイクルでB_CNTが0になることが示されている。

0062

3行目では、検証プロパティBの終わりが示されており、4行目では、上記の検証プロパティBの内容が偽と判断された場合、エラーとすることが示されている。
検証部13は、上記のような検証プロパティBを用いて、ハンドシェイクの手順を満たさない信号を出力する側の回路部の動作レベル(実使用レベル)の検証(形式検証または動的検証)を行い(ステップ16)、その結果を出力する(ステップS17)。なお、ステップS14の処理で、エラーが発生しないと判定された場合には、ハンドシェイク部23でデッドロックは発生しない旨の検証結果が出力される。

0063

ステップS16では、たとえば、以下のような検証が行われる。
たとえば、図8に示した検証プロパティBが生成された場合、A_REQ_q2がアサートされたにもかかわらずB_ACKがアサートされない条件があるということを示している。このとき検証部13は、B_ACKを出力する回路部22において、検証プロパティBを用いて、A_REQ_q2がアサートされたにもかかわらずB_ACKがアサートされない条件が回路動作時に起こり得るか検証する。

0064

検証部13は、A_REQ_q2が1の状態が1サイクル以上連続したとき、B_RSTが1でなく、回路部22がリセット状態のままである場合が回路部22の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部13は、ハンドシェイク部23でデッドロックが発生する可能性があることを検証結果として出力する。

0065

また、検証部13は、A_REQ_q2が1の状態が1サイクル以上連続したとき、回路部22のカウンタ値(B_CNT)が15のままである場合が回路部22の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部13は、ハンドシェイク部23でデッドロックが発生する可能性があることを検証結果として出力する。

0066

一方、図9に示した検証プロパティBが生成された場合、B_ACK_q2がアサートされたにもかかわらずA_REQがデアサートされない条件があるということを示している。このとき検証部13は、A_REQに変化を与える側の回路部21において、検証プロパティBを用いて、B_ACK_q2がアサートされたにもかかわらずA_REQがデアサートされない条件が回路動作時に起こり得るか検証する。

0067

検証部13は、B_ACK_q2が1の状態が1サイクル以上連続しても、A_CNTが2にならない場合が、回路部22の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部13は、ハンドシェイク部23でデッドロックが発生する可能性があることを検証結果として出力する。

0068

また、図10に示した検証プロパティBが生成された場合、A_REQ_q2がデアサートされたにもかかわらずB_ACKがデアサートされない条件があるということを示している。このとき検証部13は、B_ACKを出力する側の回路部22において、検証プロパティBを用いて、A_REQ_q2がデアサートされたにもかかわらずB_ACKがデアサートされない条件が回路動作時に起こり得るか検証する。

0069

検証部13は、A_REQ_q2が1の状態が1サイクル以上連続しても、B_CNTが0にならない場合が、回路部22の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部13は、ハンドシェイク部23でデッドロックが発生する可能性があることを検証結果として出力する。

0070

以上のように第2の実施の形態の検証装置10a及び検証方法によれば、検証プロパティAを生成して、検証することで、論理回路の非同期部分であるハンドシェイク部23の検証漏れを抑制できる。

0071

また、検証プロパティAを用いてハンドシェイク部23の検証を行い、ハンドシェイクの手順を満たさない信号があるときには、その信号を出力する側の回路部で検証プロパティBを用いて検証を行うので、検証する範囲を少なくできる。これにより、検証コストや検証時間の増大を抑制できる。

0072

また、ハンドシェイク部23のデッドロックを見逃さなくなるので、各クロックドメイン別に検証を進めることも可能となる。
なお、上記のような第1及び第2の実施の形態の検証装置10,10aは、以下のようなコンピュータにより実現可能である。

0073

図11は、本実施の形態に用いるコンピュータのハードウェアの一構成例を示す図である。
コンピュータ100は、CPU(Central Processing Unit)101によって装置全体が制御されている。CPU101には、バス108を介してRAM(Random Access Memory)102と複数の周辺機器が接続されており、検証装置10,10aの各部の機能を実現する。

0074

RAM102は、コンピュータ100の主記憶装置として使用される。RAM102には、CPU101に実行させるOS(Operating System)のプログラムやアプリケーションプログラムの少なくとも一部が一時的に格納される。また、RAM102には、CPU101による処理に用いる各種データが格納される。

0075

バス108に接続されている周辺機器としては、ハードディスクドライブ(HDD:Hard Disk Drive)103、グラフィック処理装置104、入力インタフェース105、光学ドライブ装置106、及び通信インタフェース107がある。

0076

HDD103は、内蔵したディスクに対して、磁気的にデータの書き込み及び読み出しを行う。HDD103は、コンピュータ100の二次記憶装置として使用される。HDD103には、OSのプログラム、各種検証ツールなどのアプリケーションプログラム、及び図1に示した検証対象データD1などの各種データが格納される。なお、二次記憶装置としては、フラッシュメモリなどの半導体記憶装置を使用することもできる。

0077

グラフィック処理装置104には、モニタ104aが接続されている。グラフィック処理装置104は、CPU101からの命令に従って、検証結果などの画像をモニタ104aの画面に表示させる。モニタ104aとしては、CRT(Cathode Ray Tube)を用いた表示装置液晶表示装置などがある。

0078

入力インタフェース105には、キーボード105aとマウス105bとが接続されている。入力インタフェース105は、キーボード105aやマウス105bから送られてくる信号をCPU101に送信する。なお、マウス105bは、ポインティングデバイスの一例であり、他のポインティングデバイスを使用することもできる。他のポインティングデバイスとしては、タッチパネルタブレットタッチパッドトラックボールなどがある。

0079

光学ドライブ装置106は、レーザ光などを利用して、光ディスク106aに記録されたデータの読み取りを行う。光ディスク106aは、光の反射によって読み取り可能なようにデータが記録された可搬型記録媒体である。光ディスク106aには、DVD(Digital Versatile Disc)、DVD−RAM、CD−ROM(Compact Disc Read Only Memory)、CD−R(Recordable)/RW(ReWritable)などがある。

0080

通信インタフェース107は、ネットワーク107aに接続されている。通信インタフェース107は、ネットワーク107aを介して、他のコンピュータまたは通信機器との間でデータの送受信を行う。

0081

以上のようなハードウェア構成によって、本実施の形態の処理機能を実現することができる。
また、検証装置10,10aが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータ(たとえば、図11のようなコンピュータ100)で実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、磁気記憶装置、光ディスク、光磁気記録媒体半導体メモリなどがある。磁気記憶装置には、HDD、フレキシブルディスクFD)、磁気テープなどがある。光ディスクには、DVD、DVD−RAM、CD−ROM/RWなどがある。光磁気記録媒体には、MO(Magneto-Optical disk)などがある。

0082

プログラムを流通させる場合には、たとえば、そのプログラムが記録されたDVD、CD−ROMなどの可搬型記録媒体販売される。また、プログラムをサーバコンピュータ記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。

0083

プログラムを実行するコンピュータは、たとえば、可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶装置に格納する。そして、コンピュータは、自己の記憶装置からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、ネットワークを介して接続されたサーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムにしたがった処理を実行することもできる。

0084

また、上記の処理機能の少なくとも一部を、DSP(Digital Signal Processor)、ASIC(Application Specific IntegratedCircuit)、PLD(Programmable Logic Device)などの電子回路で実現することもできる。

0085

以上、実施の形態に基づき、本発明の検証装置、検証方法及びプログラムの一観点について説明してきたが、これらは一例にすぎず、上記の記載に限定されるものではない。

0086

10検証装置
11 記憶部
12 抽出部
13 検証部
20論理回路
21,22回路部
23ハンドシェイク部
D1 検証対象データ

ページトップへ

この技術を出願した法人

この技術を発明した人物

ページトップへ

関連する挑戦したい社会課題

関連する公募課題

ページトップへ

おススメ サービス

おススメ astavisionコンテンツ

新着 最近 公開された関連が強い技術

この 技術と関連性が強い技術

関連性が強い 技術一覧

この 技術と関連性が強い人物

関連性が強い人物一覧

この 技術と関連する社会課題

関連する挑戦したい社会課題一覧

この 技術と関連する公募課題

関連する公募課題一覧

astavision 新着記事

サイト情報について

本サービスは、国が公開している情報(公開特許公報、特許整理標準化データ等)を元に構成されています。出典元のデータには一部間違いやノイズがあり、情報の正確さについては保証致しかねます。また一時的に、各データの収録範囲や更新周期によって、一部の情報が正しく表示されないことがございます。当サイトの情報を元にした諸問題、不利益等について当方は何ら責任を負いかねることを予めご承知おきのほど宜しくお願い申し上げます。

主たる情報の出典

特許情報…特許整理標準化データ(XML編)、公開特許公報、特許公報、審決公報、Patent Map Guidance System データ