アサーションベース検証装置、およびアサーションベース検証方法
【課題】大規模で複雑化した半導体集積回路に対する機能検証を効率よく実行しつつ、検証対象の半導体集積回路の品質を向上させる技術を提供する。
【解決手段】論理シミュレーション実行部（１５）（１７）の機能によって、制御可アサーション記述ファイル（２５）の、処理対象アサーション記述と処理非対象アサーション記述とを特定する。処理対象アサーション記述を用いてＤＵＴ（２２）に対するアサーションベース検証を実行しつつ、発火条件を満足したか否かを判定した結果に基づいて発火情報レジスタ（２８）を書き換える。発火情報レジスタ（２８）のデータに基づいてアサーション制御情報（２７）を更新して新たなアサーション制御情報（２７）とし、新たなアサーション制御情報（２７）を用いてアサーションベース検証を実行する。
【解決手段】論理シミュレーション実行部（１５）（１７）の機能によって、制御可アサーション記述ファイル（２５）の、処理対象アサーション記述と処理非対象アサーション記述とを特定する。処理対象アサーション記述を用いてＤＵＴ（２２）に対するアサーションベース検証を実行しつつ、発火条件を満足したか否かを判定した結果に基づいて発火情報レジスタ（２８）を書き換える。発火情報レジスタ（２８）のデータに基づいてアサーション制御情報（２７）を更新して新たなアサーション制御情報（２７）とし、新たなアサーション制御情報（２７）を用いてアサーションベース検証を実行する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、アサーションベース検証装置、およびアサーションベース検証方法に関する。
【背景技術】
【０００２】
情報処理技術の進歩に伴って、情報処理装置（コンピュータ）に搭載される半導体集積回路の大規模化が進んできている。また、情報処理装置に対する高性能化や高機能化の要求に伴って、半導体集積回路の内部の構成が、非常に複雑になってきている。
【０００３】
大規模で複雑化した半導体集積回路を適切に設計し、品質の高い製品を得るために、半導体集積回路の設計においては、機能検証などを行う検証工程に多くの時間や工数を費やしている。例えば、近年の回路設計の現場においては、機能検証にかかるＴＡＴ（Ｔｉｍｅ Ａｒｏｕｎｄ Ｔｉｍｅ）が、全体の７割近くかかるといわれている。検証工程に費やす時間や工程数の増加は、製品のコストの増大に繋がる。そのため、大規模で複雑化した半導体集積回路に対する機能検証を効率よく実行しつつ、検証対象の半導体集積回路の品質を向上させることが好ましい。大規模で複雑化した半導体集積回路の検証工程に適用される技術の一つとして、アサーションベース検証（Ａｓｓｅｒｔｉｏｎ Ｂａｓｅｄ Ｖｅｒｉｆｉｃａｔｉｏｎ）が知られている。
【０００４】
アサーションベース検証は、設計仕様に従って適切に設計されたときの回路の動作を、アサーションベース検証専用の言語（アサーション言語）で記述したアサーション記述を用いた検証である。アサーション言語には、例えば、Ｓｙｓｔｅｍ Ｖｅｒｉｌｏｇ Ａｓｓｅｒｔｉｏｎや、ＰＳＬなどがある。アサーションベース検証では、回路シミュレーションを実行しているときに、ＤＵＴ（Ｄｅｓｉｇｎ Ｕｎｄｅｒ Ｔｅｓｔ、または、Ｄｅｖｉｃｅ Ｕｎｄｅｒ Ｔｅｓｔ）の動作を、アサーション記述に基づいて常時監視し、違反したアサーション記述とその違反が発生時間を特定して通知している。
【０００５】
機能検証にアサーションベース検証を適用した場合、論理シミュレーションにかかる負荷が大きくなり、アサーションベース検証を適用していない場合に比較して、シミュレーション時間が大きくなる。そして、論理シミュレーションを行った際に発見された不具合は、その都度修正される。修正による新たな不具合が発生しているか否かを確認するために、リグレッションテスト（全テストパターンのシミュレーションを行い、不具合修正が悪い影響を与えていないことを確認する検証）が行われる。即ち、アサーションベース検証は、リグレッションテストが行われるたびに、繰り返し実行される。そのため、アサーションベース検証を適用していない場合に比較して、ＴＡＴが長くなる。アサーションベース検証を機能検証に適用した場合に、ＴＡＴを増大させないようにする技術が知られている（例えば、特許文献１、２参照。）。
【０００６】
特許文献１には、インライン付加したアサーション記述を個々に制御できる仕組みを組み込むことで、シミュレーション速度の劣化を防ぐアサーション記述言語生成方法が記載されている。そのアサーション記述言語生成方法では、対象回路の検証機能等ごとにグループ化し、アサーション記述の各行先頭部に識別子を付加する。識別子が付加された入力ファイルを読込み、シミュレーションにより動作検証する機能等のグループを指示し、この指示に基づいて入力ファイルの対応する機能等のアサーション記述を検索する。その検索により検証対象とされた機能等のアサーション記述の各行識別子を削除し、検索により検証対象外とされたアサーション記述の各行の識別子をコメント行に変更する。または、各行の記述全体を削除する。最終的に、削除または変更により変換されたアサーション記述と回路記述とで記述された出力ファイルを生成する。
【０００７】
特許文献２には、アサーションベース検証を採用した場合、ＤＵＴの誤りを見逃す可能性を警告し、検証精度の低下を防止し、無駄な検証の実施を防止する論理検証装置が開示されている。その論理検証装置は、論理システムの設計データ（ＲＴＬ）を有限状態機械（ＦＳＭ）に変換する。また、設計データの検証に用いるアサーションをアサーション記述毎に内部表現に変換する。そして、有限状態機械の状態遷移を辿り、内部表現が成立する条件に含まれる有限状態機械の状態を、内部表現毎に求め、第１の集合の元とする。また、変換された有限状態機械の動的検証をテストに従って実施し、動的検証した有限状態機械の状態をテスト毎に求め、第２の集合の元とする。その第１及び第２の集合の元として求めた状態の包含関係を判定し、その判定結果に応じて、検証を実施可能なアサーションとテストの組み合わせに分類する。
【０００８】
特許文献２に記載の論理検証装置は、第１の集合の元が空集合と判定された場合、当該アサーションを冗長なアサーションに分類し、第２の集合の元が空集合と判定された場合、当該テストに従ったシミュレーションの実施を抑止する組み合わせに分類する。
【先行技術文献】
【特許文献】
【０００９】
【特許文献１】特開２００９−１７５９３０号公報
【特許文献２】特開２００８−０３３６９０号公報
【発明の概要】
【発明が解決しようとする課題】
【００１０】
特許文献１に記載の技術では、検証機能、機能検証ブロック単位で、ユーザーがアサーション識別子を埋め込む必要がある。新規に設計された半導体集積回路であれば、アサーション作成の際に、アサーション識別子を埋め込むことで、特許文献１に記載の技術に対応することができる。
【００１１】
しかしながら、以前に設計した回路を流用した回路設計を行うときや、ＩＰコアに付随するアサーションのときには、ユーザーがアサーション識別子を埋め込むことが困難な場合がある。そのため、アサーション識別子の埋め込に時間を費やしてしまうことがある。また、１チップ検証のような大規模ＤＵＴや複雑化したＤＵＴに特許文献１に記載の技術を適用する場合、ユーザーがアサーション有効に指定した機能ブロック以外のブロックに不具合があったとしても、その不具合を発見できないことがある。
【００１２】
特許文献１に記載の技術では、アサーションベース検証を有効とする範囲や、不具合を発見することが可能な範囲は、ユーザーによってアサーション有効に指定された機能ブロックに制限されてしまう。そのため、不具合修正の後に実行されるリグレッションテストの際に、ユーザーによってアサーション有効に指定されていない機能ブロックに不具合修正に起因する新たな不具合が生じた場合、その機能ブロック（アサーション有効に指定されていない機能ブロック）に生じた新たな不具合を見つけられないことがある。
【００１３】
アサーション有効に指定されていない機能ブロックの不具合を見つけるには、ユーザーによって、改めてその機能ブロックがアサーション有効に指定されなければならず、アサーションベース検証にかかるＴＡＴが増大してしまうことがある。
【００１４】
特許文献２に記載の技術では、ＤＵＴのＲＴＬより、有限状態機械を生成し、各アサーションから変換された内部表現条件（アサーションの発火条件）を作っている。その後、その有限状態機械の動的検証を、全テストにおいて行い、各テストで通過した有限状態機械の集合を求めること必要となる。この有限状態機械の動的検証は、ＤＵＴのＲＴＬを入力とした通常の論理シミュレーションとは別に行う必要がある。そのため、アサーションベース検証にかかるＴＡＴが増大してしまうことがある。
【００１５】
また、特許文献２に記載の技術には、全テストにおいて、有限状態機械の値を入力とした論理シミュレーションを行い、各テストで通過した有限状態機械の集合を求める方法が開示されている。その方法の場合、ＲＴＬから有限状態機械を生成する際に、変換不具合が混入する可能性がある。また、ＲＴＬを入力とした通常の論理シミュレーションの代替とすることができないため、有限状態機械の集合を求めるための論理シミュレーションと、通常のＲＴＬを入力とした論理シミュレーションとを別々に実施する必要がある。そのため、アサーションベース検証にかかるＴＡＴが増大してしまうことがある。
【００１６】
本発明が解決しようとする課題は、大規模で複雑化した半導体集積回路に対する機能検証を効率よく実行しつつ、検証対象の半導体集積回路の品質を向上させる技術を提供することにある。
【課題を解決するための手段】
【００１７】
以下に、［発明を実施するための形態］で使用される番号を用いて、［課題を解決するための手段］を説明する。これらの番号は、［特許請求の範囲］の記載と［発明を実施するための形態］との対応関係を明らかにするために付加されたものである。ただし、それらの番号を、［特許請求の範囲］に記載されている発明の技術的範囲の解釈に用いてはならない。
【００１８】
上記の課題を解決するために、アサーションベース検証用の情報を記憶する記憶部（８）と、アサーションベース検証に対応した論理シミュレーションを実行する論理シミュレーション実行部（１５）（１７）としての機能を提供する演算処理部（５）とを具備するアサーションベース検証装置を構成する。ここで、前記記憶部（８）は、前記論理シミュレーションの対象であるＤＵＴ（２２）と、前記アサーションベース検証で使用されるアサーション記述に含まれる発火条件と、前記発火条件を満足したか否かに関する情報とを関連付けて記憶する発火情報レジスタ（２８）と、アサーション記述を処理対象とするか否かの設定が可能な制御可アサーション記述ファイル（２５）と、前記制御可アサーション記述ファイル（２５）の前記設定を制御するためのアサーション制御情報（２７）とを記憶することが好ましい。また、前記演算処理部（５）は、前記論理シミュレーション実行部（１５）（１７）の機能によって、前記制御可アサーション記述ファイル（２５）のアサーション記述のうち、前記アサーション制御情報（２７）によって処理対象に指定されたアサーション記述を、処理対象アサーション記述とし、前記アサーション制御情報（２７）によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述として特定し、前記処理対象アサーション記述を用いて前記ＤＵＴ（２２）に対するアサーションベース検証を実行した結果を実行ログ（３２）に記録し、前記発火条件を満足したか否かを判定した結果に基づいて前記発火情報レジスタ（２８）を書き換え、前記発火情報レジスタ（２８）のデータに基づいて発火結果ログ（３１）を生成し、前記発火結果ログ（３１）に基づいて前記アサーション制御情報（２７）を更新して新たなアサーション制御情報（２７）とし、前記新たなアサーション制御情報（２７）を用いて前記アサーションベース検証を実行する。
【発明の効果】
【００１９】
本願において開示される発明のうち、代表的なものによって得られる効果を簡単に説明すれば、大規模で複雑化した半導体集積回路に対する機能検証を効率よく実行しつつ、検証対象の半導体集積回路の品質を向上させることが可能である。
具体的には、本願のアサーションベース検証を実行することで、リグレッションテスト時は、各テストパターンにおいて、発火することが判明しているアサーション記述だけを有効にする。そのため、シミュレーションの実行ＴＡＴを短縮させることができる。
【図面の簡単な説明】
【００２０】
【図１】図１は、本実施形態のアサーションベース検証装置１の構成を例示するブロック図である。
【図２Ａ】図２Ａは、アサーション記述ファイル２１の構成を例示する図である。
【図２Ｂ】図２Ｂは、本実施形態の発火情報レジスタ２８の構成を例示する図である。
【図３Ａ】図３Ａは、アサーション記述ファイル２１の他の構成を例示する図である。
【図３Ｂ】図３Ｂは、図３Ａに例示されるプロパティ記述に対応した発火情報レジスタ２８の構成を例示する図である。
【図４】図４は、本実施形態のアサーション制御情報２７の構成を例示する図である。
【図５】図５は、本実施形態の制御可アサーション記述ファイル２５の構成を例示する図である。
【図６】図６は、本実施形態のアサーションベース検証装置１における前処置の動作を概念的に例示するブロック図である。
【図７】図７は、本実施形態のアサーションベース検証装置１におけるアサーションベース検証の動作を概念的に例示するブロック図である。
【図８】図８は、第２実施形態の制御可アサーション記述ファイル２５の構成を例示する図である。
【図９】図９は、第２実施形態のアサーションベース検証装置１におけるアサーションベース検証の動作を概念的に例示するブロック図である。
【発明を実施するための形態】
【００２１】
［第１実施形態］
以下、本発明の実施の形態を図面に基づいて説明する。なお、実施の形態を説明するための図において、同一の部材には原則として同一の符号を付し、その繰り返しの説明は省略する。
【００２２】
図１は、本実施形態のアサーションベース検証装置１の構成を例示するブロック図である。本実施形態において、アサーションベース検証装置１は、アサーションベース検証装置の機能を提供するためのプログラムを実行するコンピュータによって実現される。図１を参照すると、アサーションベース検証装置１は、情報処理装置２と、入力装置３と、出力装置４とを備えている。
【００２３】
情報処理装置２は、アサーションベース検証装置１の本体部分に相当する演算処理装置であり、プログラムに示される手順に従って情報処理を高速に実行する。本実施形態の情報処理装置２は、入力、出力、記憶、演算、制御などの基本機能を有し、アサーションベース検証装置１として機能することができる。入力装置３は、ユーザーが情報処理装置２へデータを入力するためのマンマシンインターフェースである。例えば、キーボードやマウスなどが入力装置３として例示される。出力装置４は、情報処理装置２の処理結果を外部に出力するためのマンマシンインターフェースである。例えば、ディスプレイ装置やプリンターなどが、出力装置４として例示される。
【００２４】
図１に示されているように、情報処理装置２は、ＣＰＵ５と、メモリ６と、入出力インターフェース７と、大容量記憶装置８とを備え、それらはバス９を介して情報通信可能に接続されている。ＣＰＵ５は、情報処理装置２に備えられた各種装置の制御や、データの処理を行う装置である。ＣＰＵ５は、入力装置３などを介して受け取ったデータを解釈して演算し、その演算結果を出力装置４などで出力する。本実施形態のＣＰＵ５は、大容量記憶装置８に格納された各種プログラムやデータを読み出して処理することで、情報処理装置２をアサーションベース検証装置１として機能させる。メモリ６は、データの読み出しと書き込みとが可能な記憶装置であり、情報処理装置２がソフトウェアを実行する際のメインメモリとして使用される。入出力インターフェース７は、各種装置の間のデータ通信を制御する。大容量記憶装置８は、磁気ディスクや不揮発性半導体記憶装置に代表される記憶装置である。
【００２５】
図１を参照すると、大容量記憶装置８は、前処理用プログラム１１を備えている。その前処理用プログラム１１は、本実施形態のアサーションベース検証を実行する前段階において、予備的に実行される処理（以下、前処理と記載する）の手順を示している。その前処理は、アサーションベース検証を実行する前の予備動作であり、前処理用プログラム１１を実行することで、初期状態のアサーション制御情報２７と、発火情報レジスタ２８と、制御可アサーション記述ファイル２５とを生成する。
【００２６】
前処理用プログラム１１は、アサーション制御情報生成部１２と、発火情報レジスタ生成部１３と、アサーション記述抽出部１４とを含んでいる。アサーション制御情報生成部１２は、その前処理において、初期状態のアサーション制御情報２７を生成するための手順を示している。発火情報レジスタ生成部１３は、その前処理において、発火情報レジスタ２８を生成するための手順を示している。アサーション記述抽出部１４は、予めアサーション記述ファイル２１が備えられていないときや、ＤＵＴ（ＲＴＬ）２２内にアサーション記述が含まれるときに、そのアサーション記述ファイル２１をＤＵＴ（ＲＴＬ）２２から抽出するための手順を示している。
【００２７】
また、大容量記憶装置８はアサーションベース検証プログラム１５を備えている。そのアサーションベース検証プログラム１５は、本実施形態におけるアサーションベース検証を実現するための手順を示している。アサーションベース検証プログラム１５は、コメント制御アサーション生成部１６と、論理シミュレーション実行部１７と、差分ログ生成部１８とを含んでいる。
【００２８】
コメント制御アサーション生成部１６は、コメント制御アサーション記述ファイル２９を生成するための手順を示している。論理シミュレーション実行部１７は、論理シミュレーションを行うための手順を示している。差分ログ生成部１８は、差分ログ３３を生成するための手順を示している。
【００２９】
また、大容量記憶装置８は、アサーション記述ファイル２１と、ＤＵＴ（ＲＴＬ）２２と、テストベンチ２３と、テストパターン２４と、制御可アサーション記述ファイル２５と、アサーション制御情報２７と、発火情報レジスタ２８と、コメント制御アサーション記述ファイル２９と、発火結果ログ３１と、実行ログ３２と、差分ログ３３とを格納可能に構成されている。
【００３０】
アサーション記述ファイル２１は、設計仕様に従って適切に設計されたときの回路の動作を、アサーションベース検証専用の言語（アサーション言語）で記述したアサーション記述を有するファイルである。本実施形態において、アサーション記述ファイル２１は、ＤＵＴ（ＲＴＬ）２２の記述の内部に注釈行として埋め込まれたアサーション記述を、前処理の段階で抽出されることで生成される。なお、アサーション記述ファイル２１は、独立したファイルとして予め定義されていても良い。ＤＵＴ（ＲＴＬ）２２は、検証対象の装置を表している。テストベンチ２３は、Verilog（ヴェリログ）などのハードウェア記述言語を用いて構成され、設計が正確・妥当であるかどうかを検証するための環境を提供している。テストパターン２４は、Verilog（ヴェリログ）などのハードウェア記述言語を用いて構成され、ＤＵＴの入力を制御する情報を含んでいる。テストパターン２４は、検証対象の装置が、要求された仕様にしたがって動作するか否かを検証するために用いられる。
【００３１】
制御可アサーション記述ファイル２５は、アサーション記述に対し、有効／無効を制御することができるような機能を備えている。アサーション制御情報２７は、制御可アサーション記述ファイル２５に対する有効／無効の設定を制御するために用いられる制御情報を備えている。アサーション制御情報２７の制御情報は、アサーションベース検証を実行することによって、有効／無効の設定を変更することができる。アサーション制御情報２７は、複数のテストパターン２４の各々に対応して用意され、様々なテストパターン２４に応じた動作に適したアサーション制御情報２７が使用される。
【００３２】
発火情報レジスタ２８は、アサーション記述の条件と、その条件の成立／不成立との対応関係に関する情報を備えている。発火情報レジスタ２８は、アサーション記述ファイル２１に含まれる全ての発火条件に対し、その条件の成立／不成立に関する情報を記憶する。コメント制御アサーション記述ファイル２９は、制御可アサーション記述ファイル２５に含まれる所定のアサーション記述に対し、有効／無効の設定が施されたリストを含んでいる。
【００３３】
発火結果ログ３１は、アサーション記述の条件の成立／不成立を記録している。実行ログ３２は、シミュレーションの実行結果を記録している。差分ログ３３は、発火結果ログ３１と、アサーション制御情報２７との差分を記録している。
【００３４】
図２Ａは、アサーション記述ファイル２１の構成を例示する図である。アサーション記述ファイル２１は、アサーション記述言語で構成されている。図２Ａに示されているように、アサーション記述は、設計仕様に従って適切に設計されたときの回路の動作を記述したプロパティ記述と、そのプロパティをインスタンスするassertステートメントから構成されている。具体的には、
“property”と“endproperty”
とで囲まれた文字列
“@(posedge clk)disable iff(!rst_n)a&b |=>c##1
d;”
（以下、プロパティ記述と記載する）によって、検証を行うための条件と監視する検証動作とが定義されている。図２Ａに例示されているプロパティ記述は、
“@(posedge clk) disable iff (!rst_n)a&b”
のように表された発火条件と、
“|=>c##1 d;”
のように表された検証動作とを含んでいる。
アサーションとは、上記の説明のように、プロパティ記述とそれをインスタンスするassertステートメント記述の２段構成となっている。このようなアサーションは、一般的に、コンカレント・アサーションと呼ばれることもある。本実施形態において、コンカレント・アサーションの記述方法に特別な制限は無い。例えば、コンカレント・アサーションの記述方法として、
assert property()
の()内部に直接、プロパティ記述を書く記述方法が例示される。図２Ａの記述を、上述の直接記述に直すと、
assert property(@(posedge clk) disable
iff(!rst_n)a&b |=>c##1 d);
のように表される。
【００３５】
図２Ａに例示されているプロパティ記述は、クロックのエッジが立ち上がったときに、リセット信号によるリセットがかっているか否を評価し、リセットがかかっていない場合に、信号ａと信号ｂの両方が論理１（Ｈｉｇｈレベル）となっている場合を、発火条件の成立状態としている。リセットがかかっている場合には、その処理は終了する。その発火条件の成立に応答して、
“|=>c##1 d;”
の検証を行う。図２Ａに例示されているプロパティ記述では、『信号ａと信号ｂの両方が論理１になったタイミングから、１クロック後に、信号ｃが論理１になって、更にその１クロック後に、信号ｄが論理１になるか否か』を検証する。
【００３６】
図２Ｂは、本実施形態の発火情報レジスタ２８の構成を例示する図である。発火情報レジスタ２８は、Verilog（ヴェリログ）などのハードウェア記述言語を用いて構成されている。発火情報レジスタ２８は、アサーション記述ファイル２１のプロパティ記述の発火条件と、その条件の成立／不成立示す情報とを関連付けて記憶する。本実施形態の発火情報レジスタ２８は、アサーションベース検証を含む論理シミュレーションを実行しているときに、与えられた条件を満足した発火条件に対し、レジスタ値を“１”として記憶する。
【００３７】
また、発火情報レジスタ２８は、複数のアサーション記述の数と同数の記憶領域を備えている。発火情報レジスタ２８は、その複数のアサーション記述の発火条件の各々に対し、一対一に対応する１ビットの情報を記憶する機能を備えている。図２Ｂは、クロックのエッジが立ち上がったときに、リセットがかっていない、かつ、信号ａと信号ｂの両方が論理１のときに、論理１の１ビットの情報を記憶するレジスタを表している。
【００３８】
図３Ａは、アサーション記述ファイル２１の他の構成を例示する図である。図３Ａに例示されているプロパティ記述は、クロックのエッジが立ち上がったとき、かつ、リセット信号によるリセットがかっていないときに、信号ｘが論理１になった１クロック後に信号ｙが論理１になった場合を、発火条件の成立状態としている。また、図３Ａに例示されているプロパティ記述は、その発火条件の成立に応答して、『発火条件の成立の１クロック後に、信号ｚが“１”になるか否か』を検証する。
【００３９】
図３Ｂは、図３Ａに例示されるプロパティ記述に対応した発火情報レジスタ２８の構成を例示する図である。図３Ｂは、リセット信号を１クロック遅延させた信号（遅延させたリセット信号）と、信号ｘを１クロック遅延させた信号（遅延させた信号ｘ）をラッチし、クロックのエッジが立ち上がったとき、リセットがかっていない、かつ、遅延させたリセット信号と、遅延させた信号ｘと、信号ｙとが全て論理１のときに、論理１の１ビットの情報を記憶するレジスタを表している。
【００４０】
図４は、本実施形態のアサーション制御情報２７の構成を例示する図である。アサーション制御情報２７は、アサーションベース検証を実行するときに、検証の対象としないアサーション記述を特定するための制御情報を含んでいる。図４に示されているように、アサーション制御情報２７は、複数のレコードを備えている。複数のレコードの各々は、“value”を表すフィールドと、“mem addr”を表すフィールドと、“assertion(property)name”を表すフィールドとを含んでいる。
【００４１】
“value”を表すフィールドに記載される“１”は、アサーション記述が有効とされた状態であることを示す。“value”を表すフィールドに記載される“０”は、アサーション記述が無効とされた状態であることを示す。
【００４２】
また、本実施形態のアサーションベース検証装置１は、アサーションベース検証の予備的な処理において、“value”を表すフィールドを全て“１”の状態にしたアサーション制御情報２７（初期アサーション制御情報）を生成する。アサーション制御情報２７は、複数のテストパターン２４の各々に対応して用意され、論理シミュレーション時に使用される。
【００４３】
図５は、本実施形態の制御可アサーション記述ファイル２５の構成を例示する図である。図５に示されているように、制御可アサーション記述ファイル２５は、制御用文字列
“//ast_cont_reg[0]//”
が記載されている。その制御用文字列は、assert文の上の行に記載されている。本実施形態の制御可アサーション記述ファイル２５において、そのassert文は、“：”の前にアサーション識別子を備えている。制御可アサーション記述ファイル２５のassert文を、コメント行として処理することで、アサーションベース検証を実行する際に、そのアサーション記述に関連する処理をスキップすることができる。
【００４４】
図６は、本実施形態のアサーションベース検証装置１における前処置（アサーションベース検証を行う前の段階において実行される処理）の動作を概念的に例示するブロック図である。本実施形態のアサーションベース検証装置１において、情報処理装置２のＣＰＵ５は、前処理用プログラム１１を読み出し、その前処理用プログラム１１に示される手順に従って前処理を実行することで、制御可アサーション記述ファイル２５と、アサーション制御情報２７と、発火情報レジスタ２８とを予め生成する。
【００４５】
図６に示されているように、その前処理において、アサーションベース検証装置１はアサーション記述抽出部１４によって、ＤＵＴ（ＲＴＬ）２２からアサーション記述ファイル２１を抽出する。なお、アサーション記述ファイル２１が別ファイルとして用意されている場合には、アサーション記述抽出部１４による抽出処理を省略しても良い。アサーション制御情報生成部１２は、そのアサーション記述ファイル２１を参照して、制御可アサーション記述ファイル２５と、アサーション制御情報２７を生成する。また、発火情報レジスタ生成部１３は、アサーション記述ファイル２１を参照して発火情報レジスタ２８を生成する。
【００４６】
本実施形態のアサーションベース検証装置１は、検証に初期段階で、前処理によって制御可アサーション記述ファイル２５と、アサーション制御情報２７と、発火情報レジスタ２８とを行っている。その後、アサーションベース検証を実行したときに、ＤＵＴ不具合により、ＲＴＬの修正が行われた場合でであっても、従来技術のようにＲＴＬから有限状態機械を再作成する処理を行う必要が無い。本実施形態のアサーションベース検証装置１は、アサーション記述ファイル２１に変更が無い限り、上述の前処理を再実行する必要が無い。
【００４７】
図７は、本実施形態のアサーションベース検証装置１におけるアサーションベース検証（アサーション記述に対応した論理シミュレーション）の動作を概念的に例示するブロック図である。本実施形態のアサーションベース検証装置１において、情報処理装置２のＣＰＵ５が、アサーションベース検証プログラム１５を読み出し、アサーションベース検証プログラム１５に示される手順に従って動作することで、アサーションベース検証装置としての機能を提供する。なお、以下の説明において、上述の前処理は、既に実行されたものとする。
【００４８】
アサーションベース検証を実行する場合、図７に示されているように、アサーションベース検証装置１は、コメント制御アサーション生成部１６として機能し、予め備えられたアサーション制御情報２７と、制御可アサーション記述ファイル２５と読み出す。コメント制御アサーション生成部１６は、アサーション制御情報２７の“value”に対応するフィールドのデータに基づいて、コメント制御アサーション記述ファイル２９を生成する。
【００４９】
コメント制御アサーション記述ファイル２９は、上述の図５に例示された制御可アサーション記述ファイル２５の制御用文字列
“//ast_cont_reg[0]//”
の、下の行をコメント行にすることによって生成される。コメント制御アサーション生成部１６は、アサーション制御情報２７の“value”の値を参照して、“０”が記載されていれば、制御可アサーション記述ファイル２５の対応するassert文を無効にし、“１”が記載されていれば、制御可アサーション記述ファイル２５の対応するassert文を有効にしてコメント制御アサーション記述ファイル２９とする。初回のアサーションベース検証の場合、読み出されたアサーション制御情報２７（初期アサーション制御情報）の各レコードの“value”に対応したフィールドは、全て“１”が記載されている。コメント制御アサーション生成部１６は、その初期アサーション制御情報に基づいて、制御可アサーション記述ファイル２５のassert文を全て有効状態にして、最初のアサーションベース検証用のコメント制御アサーション記述ファイル２９を生成する。
【００５０】
その後、アサーションベース検証装置１は、論理シミュレーション実行部１７として機能し、シミュレーションに用いるテストパターン２４を特定し、コメント制御アサーション記述ファイル２９に対応した論理シミュレーションを行う。このとき、論理シミュレーション実行部１７は、ＤＵＴ（ＲＴＬ）２２、テストベンチ２３、テストパターン２４、および発火情報レジスタ２８を読み出す。また、論理シミュレーション実行部１７は、コメント制御アサーション記述ファイル２９を読み出す。
【００５１】
論理シミュレーション実行部１７は、論理シミュレーションを実行しているときに、コメント制御アサーション記述ファイル２９に含まれるアサーション記述の発火条件と同等な論理である発火情報レジスタ２８のif節を満足するか否かを判断する。このとき、論理シミュレーション実行部１７は、コメント制御アサーション記述ファイル２９に含まれるアサーション記述が、有効か無効かに依存することなく、全ての記述の発火条件と同等な論理である発火情報レジスタ２８のif節を満足するか否かを判断する。論理シミュレーション実行部１７は、その判断の結果に基づいて、条件を満足したif節に対応する発火情報レジスタ２８のレジスタ値を“１”にする。また、論理シミュレーション実行部１７は、与えられた条件を満足しなかった発火条件に対応する発火情報レジスタ２８に対しては何も処理をしないため、初期値“ｘ（不定）”のままである。発火情報レジスタ２８が、Verilog（ヴェリログ）などのハードウェア記述言語を用いて構成されているため、論理シミュレーション実行部１７は、発火情報レジスタ２８のif節の成立／不成立を高速に判定することが可能である。
【００５２】
論理シミュレーション実行部１７は、論理シミュレーションを実行した実行結果を、実行ログ３２として出力する。また、論理シミュレーション実行部１７は、論理シミュレーションが終了した後、発火情報レジスタ２８の値に基づいて、アサーション制御情報２７と同じファイルフォーマットの発火結果ログ３１を生成する。このとき、発火情報レジスタ２８の値が、“ｘ（不定）”である場合は、“０”に置き換えて発火結果ログ３１を生成する。論理シミュレーション実行部１７は、発火結果ログ３１をそのまま、アサーション制御情報２７として更新する。更新されたアサーション制御情報２７は、次回のアサーションベース検証に使用される。
【００５３】
実行ログ３２にアサーションエラー情報が含まれるとき、ＤＵＴ（ＲＴＬ）２２は、そのアサーションエラー情報に対応して、ＤＵＴ（ＲＴＬ）２２の解析や不具合修正が施される。アサーションベース検証装置１は、上述の発火結果ログ３１を新たなアサーション制御情報２７として用いて、修正されたＤＵＴ（ＲＴＬ）２２に対応するアサーションベース検証を実行する。
【００５４】
２回目（若しくはそれ以降）のアサーションベース検証を実行する場合、“value”に対応したフィールドに、“０”が記載されているレコードを含むアサーション制御情報２７が用いられる。コメント制御アサーション生成部１６は、そのアサーション制御情報２７に基づいて、新たなコメント制御アサーション記述ファイル２９を生成する。論理シミュレーション実行部１７は、２回目の以降のアサーションベース検証において、検証の対象外とされたアサーション記述をスキップして、アサーションベース検証に対応した論理シミュレーションを実行する。
【００５５】
このとき、論理シミュレーション実行部１７は、発火情報レジスタ２８によって、全ての発火条件に対し、その条件の成立／不成立に関する情報を記憶する。発火情報レジスタ２８が、全ての発火条件に関する情報を記憶しているので、修正されたＤＵＴ（ＲＴＬ）２２に対する検証の結果、前回の論理シミュレーションでは、条件が成立しなかった発火条件が、今回の論理シミュレーションで成立した場合、その情報は、今回出力される発火情報レジスタ２８に記憶される。
【００５６】
アサーションベース検証装置１は、論理シミュレーション実行部１７による論理シミュレーションが終了した後、差分ログ生成部１８として機能する。差分ログ生成部１８は、発火結果ログ３１と、アサーション制御情報２７とを読み出し、それらの差分を抽出する処理を行う。差分ログ生成部１８によって、発火結果ログ３１とアサーション制御情報２７との差分を抽出し、差分ログ３３を生成することで、ユーザーは、不具合を修正したことによって、新たな動作の変化を迅速に把握することができる。
【００５７】
例えば、２回目の論理シミュレーションで発火情報レジスタ２８が更新された場合、その発火情報レジスタ２８に対応した発火結果ログ３１が出力される。その発火結果ログ３１と、入力に用いたアサーション制御情報２７とを比較することで、無効にされていたアサーションが、実際には有効にすべきであるか否かの判断を行うことが可能となる。
【００５８】
また、発火結果ログ３１とアサーション制御情報２７とに差分がない場合や、無効であったアサーション記述に対し、ユーザーが手動で有効にした箇所のみが差分として記録される場合には、アサーションエラー情報に対応した不具合の修正後においても、新たに有効にすべきアサーションはなかった、つまり十分なアサーション記述を用いて論理シミュレーションを行ったと判断することが可能である。
【００５９】
しかし、それ以外の差分が生じている場合には、アサーションエラー情報に対応して不具合を修正したことにより、修正箇所以外の動作が変化していたり、同じテストパタンでも、前回と異なるタイミングで動作していたりする可能性がある。ユーザーは、差分ログ３３を参照することによって、そのような状況を迅速に発見することが可能となる。
【００６０】
本実施形態のアサーションベース検証装置１において、アサーション制御情報２７は、複数のテストパターン２４の各々に対応して用意されていることが好ましい。アサーション制御情報２７は、上述の前処理によって、各テストパターン分のアサーション制御情報２７が生成される。１回目のアサーションベース検証を行う場合には、使用するテストパターンに対応した初期状態のアサーション制御情報２７を特定して使用する。２回目以降のアサーションベース検証では、発火結果ログ３１に基づいた新たなアサーション制御情報２７を使用することで、発火条件が成立するアサーション記述のみを検証の対象とし、検証の対象外のアサーション記述をスキップすることができる。
【００６１】
なお、アサーション制御情報２７は、ユーザーが手動で有効／無効の情報を変更することが可能である。例えば、機能単位で有効にしたい場合や、特定のアサーション記述を常時有効に設定しておきたい場合などに、対応するアサーション記述に対し、アサーション制御情報２７の“value”の設定を個別に変更・修正してもよい。
【００６２】
また、複数のテストパターン２４の全ての発火結果ログ３１の総和を取ることで、一度も条件の成立がなかった発火条件を含むアサーション記述を見つけることができる。ユーザーは、一度も条件の成立がなかった発火条件を含むアサーション記述が見つかった場合、そのアサーション記述が、不要なアサーション記述であるのか、記述に間違いがあるアサーション記述なのかなどの判断を行うことができる。その判断の結果、不要なアサーション記述ならば削除し、記述の間違いであるならば修正することで、ＴＡＴを短縮しつつ品質の向上に務めることができる。
【００６３】
本実施形態のアサーションベース検証装置１による実行ＴＡＴの削減は、大規模回路やチップ全体のシミュレーションなどで、対象となるアサーション記述が多い場合に、より大きな効果を奏することができる。また、テストパターンに依存して、動作していない回路部分が大きい場合にも、より大きな効果を奏することができる。
【００６４】
［第２実施形態］
以下に、図面を参照して本願発明のアサーションベース検証装置１の第２実施形態について説明を行う。第２実施形態のアサーションベース検証装置１は、論理シミュレーションを実行する前に、制御可アサーション記述ファイル２５を生成する。その制御可アサーション記述ファイル２５は、アサーション記述ファイル２１のプロパティ記述のdisable iff節の条件文に対して、評価無効とするための条件を追加する処理をすることで生成される。それによって、第２実施形態のアサーションベース検証装置１は、コメント制御アサーション生成部１６によって生成されるコメント制御アサーション記述ファイル２９を用いることなく、アサーション記述の有効／無効を制御する。
【００６５】
図８は、第２実施形態の制御可アサーション記述ファイル２５の構成を例示する図である。第２実施形態の制御可アサーション記述ファイル２５は、アサーション制御情報生成部１２によって、アサーション記述ファイル２１の
“property”
と
“endproperty”
とで囲まれたプロパティ記述のdisable iff節の条件に、アサーション制御情報２７の“value”の値を格納したレジスタast_cont_reg[0:AST_NUM-1]の対応する１ビットを追加した形で生成される。また、同時に、ast_cont_reg[0:AST_NUM-1]というレジスタ、及び、論理シミュレーション開始時にアサーション制御情報２７の“value”の値をこのレジスタにロードするテストベンチ記述が生成される。これによって、論理シミュレーション実行時に、アサーション制御情報２７の値を格納するレジスタ
ast_cont_reg[0:AST_NUM-1]
にアサーション制御情報２７をロードするだけで、制御可アサーション記述ファイル２５のアサーション記述の有効／無効を制御することができる。図８に示されているように、制御可アサーション記述ファイル２５の、disable iff節の“（!rst_n|!ast_cont_reg[0]）”の内部が真であれば、処理は終了する。具体的には、ast_cont_reg[0]の値が０であるならば処理は終了する。
【００６６】
図９は、第２実施形態のアサーションベース検証装置１におけるアサーションベース検証（アサーション記述に対応した論理シミュレーション）の動作を概念的に例示するブロック図である。第２実施形態のアサーションベース検証装置１は、コメント制御アサーション生成部１６として機能することなく処理を行う。図９に示されているように、アサーションベース検証装置１は、論理シミュレーション実行部１７として機能し、制御可アサーション記述ファイル２５と、アサーション制御情報２７と、テストベンチ２３と、テストパターン２４と、ＤＵＴ（ＲＴＬ）２２と、発火情報レジスタ２８とを読み出す。
【００６７】
第２実施形態のアサーションベース検証装置１における論理シミュレーション実行部１７は、シミュレーションに用いるテストパターン２４を特定し、disable iff節に条件が追加された制御可アサーション記述ファイル２５に対応した論理シミュレーションを行う。このとき、論理シミュレーション実行部１７は、ＤＵＴ（ＲＴＬ）２２、テストベンチ２３、テストパターン２４、および発火情報レジスタ２８を読み出す。また、論理シミュレーション実行部１７は、アサーション制御情報２７と制御可アサーション記述ファイル２５を読み出す。このとき、論理シミュレーション実行部１７は、そのアサーション制御情報２７の値を用いて、制御可アサーション記述ファイル２５のdisable iff節の、“（!rst_n|!ast_cont_reg[0]）”の内部が真となるアサーション記述を評価無効として、アサーション記述に対応した論理シミュレーションを実行する。これによって、第１実施形態のような、無効にされたassert文を含むコメント制御アサーション記述ファイル２９を使用した場合と同様に、アサーションベース検証を実行する際に、評価無効のアサーション記述に関連する処理をスキップすることができる。その後、アサーション記述に対応した論理シミュレーションを実行した結果として、発火結果ログ３１、実行ログ３２、差分ログ３３を生成する。
【００６８】
第２実施形態のアサーションベース検証装置１は、コメント制御アサーション記述ファイル２９を生成するための処理を行うことなく、アサーションベース検証を実現している。これによって、品質を低下させることなくシミュレーションの実行ＴＡＴを短縮することが可能である。
【００６９】
以上、本願発明の実施の形態を具体的に説明した。本願発明は上述の実施の形態に限定されるものではなく、その要旨を逸脱しない範囲で種々変更可能である。また、上述の複数の実施形態は、その構成・動作に矛盾が生じない範囲において組み合わせて実施することが可能である。
【符号の説明】
【００７０】
１…アサーションベース検証装置
２…情報処理装置
３…入力装置
４…出力装置
５…ＣＰＵ
６…メモリ
７…入出力インターフェース
８…大容量記憶装置
９…バス
１１…前処理用プログラム
１２…アサーション制御情報生成部
１３…発火情報レジスタ生成部
１４…アサーション記述抽出部
１５…アサーションベース検証プログラム
１６…コメント制御アサーション生成部
１７…論理シミュレーション実行部
１８…差分ログ生成部
２１…アサーション記述ファイル
２２…ＤＵＴ（ＲＴＬ）
２３…テストベンチ
２４…テストパターン
２５…制御可アサーション記述ファイル
２７…アサーション制御情報
２８…発火情報レジスタ
２９…コメント制御アサーション記述ファイル
３１…発火結果ログ
３２…実行ログ
３３…差分ログ
【技術分野】
【０００１】
本発明は、アサーションベース検証装置、およびアサーションベース検証方法に関する。
【背景技術】
【０００２】
情報処理技術の進歩に伴って、情報処理装置（コンピュータ）に搭載される半導体集積回路の大規模化が進んできている。また、情報処理装置に対する高性能化や高機能化の要求に伴って、半導体集積回路の内部の構成が、非常に複雑になってきている。
【０００３】
大規模で複雑化した半導体集積回路を適切に設計し、品質の高い製品を得るために、半導体集積回路の設計においては、機能検証などを行う検証工程に多くの時間や工数を費やしている。例えば、近年の回路設計の現場においては、機能検証にかかるＴＡＴ（Ｔｉｍｅ Ａｒｏｕｎｄ Ｔｉｍｅ）が、全体の７割近くかかるといわれている。検証工程に費やす時間や工程数の増加は、製品のコストの増大に繋がる。そのため、大規模で複雑化した半導体集積回路に対する機能検証を効率よく実行しつつ、検証対象の半導体集積回路の品質を向上させることが好ましい。大規模で複雑化した半導体集積回路の検証工程に適用される技術の一つとして、アサーションベース検証（Ａｓｓｅｒｔｉｏｎ Ｂａｓｅｄ Ｖｅｒｉｆｉｃａｔｉｏｎ）が知られている。
【０００４】
アサーションベース検証は、設計仕様に従って適切に設計されたときの回路の動作を、アサーションベース検証専用の言語（アサーション言語）で記述したアサーション記述を用いた検証である。アサーション言語には、例えば、Ｓｙｓｔｅｍ Ｖｅｒｉｌｏｇ Ａｓｓｅｒｔｉｏｎや、ＰＳＬなどがある。アサーションベース検証では、回路シミュレーションを実行しているときに、ＤＵＴ（Ｄｅｓｉｇｎ Ｕｎｄｅｒ Ｔｅｓｔ、または、Ｄｅｖｉｃｅ Ｕｎｄｅｒ Ｔｅｓｔ）の動作を、アサーション記述に基づいて常時監視し、違反したアサーション記述とその違反が発生時間を特定して通知している。
【０００５】
機能検証にアサーションベース検証を適用した場合、論理シミュレーションにかかる負荷が大きくなり、アサーションベース検証を適用していない場合に比較して、シミュレーション時間が大きくなる。そして、論理シミュレーションを行った際に発見された不具合は、その都度修正される。修正による新たな不具合が発生しているか否かを確認するために、リグレッションテスト（全テストパターンのシミュレーションを行い、不具合修正が悪い影響を与えていないことを確認する検証）が行われる。即ち、アサーションベース検証は、リグレッションテストが行われるたびに、繰り返し実行される。そのため、アサーションベース検証を適用していない場合に比較して、ＴＡＴが長くなる。アサーションベース検証を機能検証に適用した場合に、ＴＡＴを増大させないようにする技術が知られている（例えば、特許文献１、２参照。）。
【０００６】
特許文献１には、インライン付加したアサーション記述を個々に制御できる仕組みを組み込むことで、シミュレーション速度の劣化を防ぐアサーション記述言語生成方法が記載されている。そのアサーション記述言語生成方法では、対象回路の検証機能等ごとにグループ化し、アサーション記述の各行先頭部に識別子を付加する。識別子が付加された入力ファイルを読込み、シミュレーションにより動作検証する機能等のグループを指示し、この指示に基づいて入力ファイルの対応する機能等のアサーション記述を検索する。その検索により検証対象とされた機能等のアサーション記述の各行識別子を削除し、検索により検証対象外とされたアサーション記述の各行の識別子をコメント行に変更する。または、各行の記述全体を削除する。最終的に、削除または変更により変換されたアサーション記述と回路記述とで記述された出力ファイルを生成する。
【０００７】
特許文献２には、アサーションベース検証を採用した場合、ＤＵＴの誤りを見逃す可能性を警告し、検証精度の低下を防止し、無駄な検証の実施を防止する論理検証装置が開示されている。その論理検証装置は、論理システムの設計データ（ＲＴＬ）を有限状態機械（ＦＳＭ）に変換する。また、設計データの検証に用いるアサーションをアサーション記述毎に内部表現に変換する。そして、有限状態機械の状態遷移を辿り、内部表現が成立する条件に含まれる有限状態機械の状態を、内部表現毎に求め、第１の集合の元とする。また、変換された有限状態機械の動的検証をテストに従って実施し、動的検証した有限状態機械の状態をテスト毎に求め、第２の集合の元とする。その第１及び第２の集合の元として求めた状態の包含関係を判定し、その判定結果に応じて、検証を実施可能なアサーションとテストの組み合わせに分類する。
【０００８】
特許文献２に記載の論理検証装置は、第１の集合の元が空集合と判定された場合、当該アサーションを冗長なアサーションに分類し、第２の集合の元が空集合と判定された場合、当該テストに従ったシミュレーションの実施を抑止する組み合わせに分類する。
【先行技術文献】
【特許文献】
【０００９】
【特許文献１】特開２００９−１７５９３０号公報
【特許文献２】特開２００８−０３３６９０号公報
【発明の概要】
【発明が解決しようとする課題】
【００１０】
特許文献１に記載の技術では、検証機能、機能検証ブロック単位で、ユーザーがアサーション識別子を埋め込む必要がある。新規に設計された半導体集積回路であれば、アサーション作成の際に、アサーション識別子を埋め込むことで、特許文献１に記載の技術に対応することができる。
【００１１】
しかしながら、以前に設計した回路を流用した回路設計を行うときや、ＩＰコアに付随するアサーションのときには、ユーザーがアサーション識別子を埋め込むことが困難な場合がある。そのため、アサーション識別子の埋め込に時間を費やしてしまうことがある。また、１チップ検証のような大規模ＤＵＴや複雑化したＤＵＴに特許文献１に記載の技術を適用する場合、ユーザーがアサーション有効に指定した機能ブロック以外のブロックに不具合があったとしても、その不具合を発見できないことがある。
【００１２】
特許文献１に記載の技術では、アサーションベース検証を有効とする範囲や、不具合を発見することが可能な範囲は、ユーザーによってアサーション有効に指定された機能ブロックに制限されてしまう。そのため、不具合修正の後に実行されるリグレッションテストの際に、ユーザーによってアサーション有効に指定されていない機能ブロックに不具合修正に起因する新たな不具合が生じた場合、その機能ブロック（アサーション有効に指定されていない機能ブロック）に生じた新たな不具合を見つけられないことがある。
【００１３】
アサーション有効に指定されていない機能ブロックの不具合を見つけるには、ユーザーによって、改めてその機能ブロックがアサーション有効に指定されなければならず、アサーションベース検証にかかるＴＡＴが増大してしまうことがある。
【００１４】
特許文献２に記載の技術では、ＤＵＴのＲＴＬより、有限状態機械を生成し、各アサーションから変換された内部表現条件（アサーションの発火条件）を作っている。その後、その有限状態機械の動的検証を、全テストにおいて行い、各テストで通過した有限状態機械の集合を求めること必要となる。この有限状態機械の動的検証は、ＤＵＴのＲＴＬを入力とした通常の論理シミュレーションとは別に行う必要がある。そのため、アサーションベース検証にかかるＴＡＴが増大してしまうことがある。
【００１５】
また、特許文献２に記載の技術には、全テストにおいて、有限状態機械の値を入力とした論理シミュレーションを行い、各テストで通過した有限状態機械の集合を求める方法が開示されている。その方法の場合、ＲＴＬから有限状態機械を生成する際に、変換不具合が混入する可能性がある。また、ＲＴＬを入力とした通常の論理シミュレーションの代替とすることができないため、有限状態機械の集合を求めるための論理シミュレーションと、通常のＲＴＬを入力とした論理シミュレーションとを別々に実施する必要がある。そのため、アサーションベース検証にかかるＴＡＴが増大してしまうことがある。
【００１６】
本発明が解決しようとする課題は、大規模で複雑化した半導体集積回路に対する機能検証を効率よく実行しつつ、検証対象の半導体集積回路の品質を向上させる技術を提供することにある。
【課題を解決するための手段】
【００１７】
以下に、［発明を実施するための形態］で使用される番号を用いて、［課題を解決するための手段］を説明する。これらの番号は、［特許請求の範囲］の記載と［発明を実施するための形態］との対応関係を明らかにするために付加されたものである。ただし、それらの番号を、［特許請求の範囲］に記載されている発明の技術的範囲の解釈に用いてはならない。
【００１８】
上記の課題を解決するために、アサーションベース検証用の情報を記憶する記憶部（８）と、アサーションベース検証に対応した論理シミュレーションを実行する論理シミュレーション実行部（１５）（１７）としての機能を提供する演算処理部（５）とを具備するアサーションベース検証装置を構成する。ここで、前記記憶部（８）は、前記論理シミュレーションの対象であるＤＵＴ（２２）と、前記アサーションベース検証で使用されるアサーション記述に含まれる発火条件と、前記発火条件を満足したか否かに関する情報とを関連付けて記憶する発火情報レジスタ（２８）と、アサーション記述を処理対象とするか否かの設定が可能な制御可アサーション記述ファイル（２５）と、前記制御可アサーション記述ファイル（２５）の前記設定を制御するためのアサーション制御情報（２７）とを記憶することが好ましい。また、前記演算処理部（５）は、前記論理シミュレーション実行部（１５）（１７）の機能によって、前記制御可アサーション記述ファイル（２５）のアサーション記述のうち、前記アサーション制御情報（２７）によって処理対象に指定されたアサーション記述を、処理対象アサーション記述とし、前記アサーション制御情報（２７）によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述として特定し、前記処理対象アサーション記述を用いて前記ＤＵＴ（２２）に対するアサーションベース検証を実行した結果を実行ログ（３２）に記録し、前記発火条件を満足したか否かを判定した結果に基づいて前記発火情報レジスタ（２８）を書き換え、前記発火情報レジスタ（２８）のデータに基づいて発火結果ログ（３１）を生成し、前記発火結果ログ（３１）に基づいて前記アサーション制御情報（２７）を更新して新たなアサーション制御情報（２７）とし、前記新たなアサーション制御情報（２７）を用いて前記アサーションベース検証を実行する。
【発明の効果】
【００１９】
本願において開示される発明のうち、代表的なものによって得られる効果を簡単に説明すれば、大規模で複雑化した半導体集積回路に対する機能検証を効率よく実行しつつ、検証対象の半導体集積回路の品質を向上させることが可能である。
具体的には、本願のアサーションベース検証を実行することで、リグレッションテスト時は、各テストパターンにおいて、発火することが判明しているアサーション記述だけを有効にする。そのため、シミュレーションの実行ＴＡＴを短縮させることができる。
【図面の簡単な説明】
【００２０】
【図１】図１は、本実施形態のアサーションベース検証装置１の構成を例示するブロック図である。
【図２Ａ】図２Ａは、アサーション記述ファイル２１の構成を例示する図である。
【図２Ｂ】図２Ｂは、本実施形態の発火情報レジスタ２８の構成を例示する図である。
【図３Ａ】図３Ａは、アサーション記述ファイル２１の他の構成を例示する図である。
【図３Ｂ】図３Ｂは、図３Ａに例示されるプロパティ記述に対応した発火情報レジスタ２８の構成を例示する図である。
【図４】図４は、本実施形態のアサーション制御情報２７の構成を例示する図である。
【図５】図５は、本実施形態の制御可アサーション記述ファイル２５の構成を例示する図である。
【図６】図６は、本実施形態のアサーションベース検証装置１における前処置の動作を概念的に例示するブロック図である。
【図７】図７は、本実施形態のアサーションベース検証装置１におけるアサーションベース検証の動作を概念的に例示するブロック図である。
【図８】図８は、第２実施形態の制御可アサーション記述ファイル２５の構成を例示する図である。
【図９】図９は、第２実施形態のアサーションベース検証装置１におけるアサーションベース検証の動作を概念的に例示するブロック図である。
【発明を実施するための形態】
【００２１】
［第１実施形態］
以下、本発明の実施の形態を図面に基づいて説明する。なお、実施の形態を説明するための図において、同一の部材には原則として同一の符号を付し、その繰り返しの説明は省略する。
【００２２】
図１は、本実施形態のアサーションベース検証装置１の構成を例示するブロック図である。本実施形態において、アサーションベース検証装置１は、アサーションベース検証装置の機能を提供するためのプログラムを実行するコンピュータによって実現される。図１を参照すると、アサーションベース検証装置１は、情報処理装置２と、入力装置３と、出力装置４とを備えている。
【００２３】
情報処理装置２は、アサーションベース検証装置１の本体部分に相当する演算処理装置であり、プログラムに示される手順に従って情報処理を高速に実行する。本実施形態の情報処理装置２は、入力、出力、記憶、演算、制御などの基本機能を有し、アサーションベース検証装置１として機能することができる。入力装置３は、ユーザーが情報処理装置２へデータを入力するためのマンマシンインターフェースである。例えば、キーボードやマウスなどが入力装置３として例示される。出力装置４は、情報処理装置２の処理結果を外部に出力するためのマンマシンインターフェースである。例えば、ディスプレイ装置やプリンターなどが、出力装置４として例示される。
【００２４】
図１に示されているように、情報処理装置２は、ＣＰＵ５と、メモリ６と、入出力インターフェース７と、大容量記憶装置８とを備え、それらはバス９を介して情報通信可能に接続されている。ＣＰＵ５は、情報処理装置２に備えられた各種装置の制御や、データの処理を行う装置である。ＣＰＵ５は、入力装置３などを介して受け取ったデータを解釈して演算し、その演算結果を出力装置４などで出力する。本実施形態のＣＰＵ５は、大容量記憶装置８に格納された各種プログラムやデータを読み出して処理することで、情報処理装置２をアサーションベース検証装置１として機能させる。メモリ６は、データの読み出しと書き込みとが可能な記憶装置であり、情報処理装置２がソフトウェアを実行する際のメインメモリとして使用される。入出力インターフェース７は、各種装置の間のデータ通信を制御する。大容量記憶装置８は、磁気ディスクや不揮発性半導体記憶装置に代表される記憶装置である。
【００２５】
図１を参照すると、大容量記憶装置８は、前処理用プログラム１１を備えている。その前処理用プログラム１１は、本実施形態のアサーションベース検証を実行する前段階において、予備的に実行される処理（以下、前処理と記載する）の手順を示している。その前処理は、アサーションベース検証を実行する前の予備動作であり、前処理用プログラム１１を実行することで、初期状態のアサーション制御情報２７と、発火情報レジスタ２８と、制御可アサーション記述ファイル２５とを生成する。
【００２６】
前処理用プログラム１１は、アサーション制御情報生成部１２と、発火情報レジスタ生成部１３と、アサーション記述抽出部１４とを含んでいる。アサーション制御情報生成部１２は、その前処理において、初期状態のアサーション制御情報２７を生成するための手順を示している。発火情報レジスタ生成部１３は、その前処理において、発火情報レジスタ２８を生成するための手順を示している。アサーション記述抽出部１４は、予めアサーション記述ファイル２１が備えられていないときや、ＤＵＴ（ＲＴＬ）２２内にアサーション記述が含まれるときに、そのアサーション記述ファイル２１をＤＵＴ（ＲＴＬ）２２から抽出するための手順を示している。
【００２７】
また、大容量記憶装置８はアサーションベース検証プログラム１５を備えている。そのアサーションベース検証プログラム１５は、本実施形態におけるアサーションベース検証を実現するための手順を示している。アサーションベース検証プログラム１５は、コメント制御アサーション生成部１６と、論理シミュレーション実行部１７と、差分ログ生成部１８とを含んでいる。
【００２８】
コメント制御アサーション生成部１６は、コメント制御アサーション記述ファイル２９を生成するための手順を示している。論理シミュレーション実行部１７は、論理シミュレーションを行うための手順を示している。差分ログ生成部１８は、差分ログ３３を生成するための手順を示している。
【００２９】
また、大容量記憶装置８は、アサーション記述ファイル２１と、ＤＵＴ（ＲＴＬ）２２と、テストベンチ２３と、テストパターン２４と、制御可アサーション記述ファイル２５と、アサーション制御情報２７と、発火情報レジスタ２８と、コメント制御アサーション記述ファイル２９と、発火結果ログ３１と、実行ログ３２と、差分ログ３３とを格納可能に構成されている。
【００３０】
アサーション記述ファイル２１は、設計仕様に従って適切に設計されたときの回路の動作を、アサーションベース検証専用の言語（アサーション言語）で記述したアサーション記述を有するファイルである。本実施形態において、アサーション記述ファイル２１は、ＤＵＴ（ＲＴＬ）２２の記述の内部に注釈行として埋め込まれたアサーション記述を、前処理の段階で抽出されることで生成される。なお、アサーション記述ファイル２１は、独立したファイルとして予め定義されていても良い。ＤＵＴ（ＲＴＬ）２２は、検証対象の装置を表している。テストベンチ２３は、Verilog（ヴェリログ）などのハードウェア記述言語を用いて構成され、設計が正確・妥当であるかどうかを検証するための環境を提供している。テストパターン２４は、Verilog（ヴェリログ）などのハードウェア記述言語を用いて構成され、ＤＵＴの入力を制御する情報を含んでいる。テストパターン２４は、検証対象の装置が、要求された仕様にしたがって動作するか否かを検証するために用いられる。
【００３１】
制御可アサーション記述ファイル２５は、アサーション記述に対し、有効／無効を制御することができるような機能を備えている。アサーション制御情報２７は、制御可アサーション記述ファイル２５に対する有効／無効の設定を制御するために用いられる制御情報を備えている。アサーション制御情報２７の制御情報は、アサーションベース検証を実行することによって、有効／無効の設定を変更することができる。アサーション制御情報２７は、複数のテストパターン２４の各々に対応して用意され、様々なテストパターン２４に応じた動作に適したアサーション制御情報２７が使用される。
【００３２】
発火情報レジスタ２８は、アサーション記述の条件と、その条件の成立／不成立との対応関係に関する情報を備えている。発火情報レジスタ２８は、アサーション記述ファイル２１に含まれる全ての発火条件に対し、その条件の成立／不成立に関する情報を記憶する。コメント制御アサーション記述ファイル２９は、制御可アサーション記述ファイル２５に含まれる所定のアサーション記述に対し、有効／無効の設定が施されたリストを含んでいる。
【００３３】
発火結果ログ３１は、アサーション記述の条件の成立／不成立を記録している。実行ログ３２は、シミュレーションの実行結果を記録している。差分ログ３３は、発火結果ログ３１と、アサーション制御情報２７との差分を記録している。
【００３４】
図２Ａは、アサーション記述ファイル２１の構成を例示する図である。アサーション記述ファイル２１は、アサーション記述言語で構成されている。図２Ａに示されているように、アサーション記述は、設計仕様に従って適切に設計されたときの回路の動作を記述したプロパティ記述と、そのプロパティをインスタンスするassertステートメントから構成されている。具体的には、
“property”と“endproperty”
とで囲まれた文字列
“@(posedge clk)disable iff(!rst_n)a&b |=>c##1
d;”
（以下、プロパティ記述と記載する）によって、検証を行うための条件と監視する検証動作とが定義されている。図２Ａに例示されているプロパティ記述は、
“@(posedge clk) disable iff (!rst_n)a&b”
のように表された発火条件と、
“|=>c##1 d;”
のように表された検証動作とを含んでいる。
アサーションとは、上記の説明のように、プロパティ記述とそれをインスタンスするassertステートメント記述の２段構成となっている。このようなアサーションは、一般的に、コンカレント・アサーションと呼ばれることもある。本実施形態において、コンカレント・アサーションの記述方法に特別な制限は無い。例えば、コンカレント・アサーションの記述方法として、
assert property()
の()内部に直接、プロパティ記述を書く記述方法が例示される。図２Ａの記述を、上述の直接記述に直すと、
assert property(@(posedge clk) disable
iff(!rst_n)a&b |=>c##1 d);
のように表される。
【００３５】
図２Ａに例示されているプロパティ記述は、クロックのエッジが立ち上がったときに、リセット信号によるリセットがかっているか否を評価し、リセットがかかっていない場合に、信号ａと信号ｂの両方が論理１（Ｈｉｇｈレベル）となっている場合を、発火条件の成立状態としている。リセットがかかっている場合には、その処理は終了する。その発火条件の成立に応答して、
“|=>c##1 d;”
の検証を行う。図２Ａに例示されているプロパティ記述では、『信号ａと信号ｂの両方が論理１になったタイミングから、１クロック後に、信号ｃが論理１になって、更にその１クロック後に、信号ｄが論理１になるか否か』を検証する。
【００３６】
図２Ｂは、本実施形態の発火情報レジスタ２８の構成を例示する図である。発火情報レジスタ２８は、Verilog（ヴェリログ）などのハードウェア記述言語を用いて構成されている。発火情報レジスタ２８は、アサーション記述ファイル２１のプロパティ記述の発火条件と、その条件の成立／不成立示す情報とを関連付けて記憶する。本実施形態の発火情報レジスタ２８は、アサーションベース検証を含む論理シミュレーションを実行しているときに、与えられた条件を満足した発火条件に対し、レジスタ値を“１”として記憶する。
【００３７】
また、発火情報レジスタ２８は、複数のアサーション記述の数と同数の記憶領域を備えている。発火情報レジスタ２８は、その複数のアサーション記述の発火条件の各々に対し、一対一に対応する１ビットの情報を記憶する機能を備えている。図２Ｂは、クロックのエッジが立ち上がったときに、リセットがかっていない、かつ、信号ａと信号ｂの両方が論理１のときに、論理１の１ビットの情報を記憶するレジスタを表している。
【００３８】
図３Ａは、アサーション記述ファイル２１の他の構成を例示する図である。図３Ａに例示されているプロパティ記述は、クロックのエッジが立ち上がったとき、かつ、リセット信号によるリセットがかっていないときに、信号ｘが論理１になった１クロック後に信号ｙが論理１になった場合を、発火条件の成立状態としている。また、図３Ａに例示されているプロパティ記述は、その発火条件の成立に応答して、『発火条件の成立の１クロック後に、信号ｚが“１”になるか否か』を検証する。
【００３９】
図３Ｂは、図３Ａに例示されるプロパティ記述に対応した発火情報レジスタ２８の構成を例示する図である。図３Ｂは、リセット信号を１クロック遅延させた信号（遅延させたリセット信号）と、信号ｘを１クロック遅延させた信号（遅延させた信号ｘ）をラッチし、クロックのエッジが立ち上がったとき、リセットがかっていない、かつ、遅延させたリセット信号と、遅延させた信号ｘと、信号ｙとが全て論理１のときに、論理１の１ビットの情報を記憶するレジスタを表している。
【００４０】
図４は、本実施形態のアサーション制御情報２７の構成を例示する図である。アサーション制御情報２７は、アサーションベース検証を実行するときに、検証の対象としないアサーション記述を特定するための制御情報を含んでいる。図４に示されているように、アサーション制御情報２７は、複数のレコードを備えている。複数のレコードの各々は、“value”を表すフィールドと、“mem addr”を表すフィールドと、“assertion(property)name”を表すフィールドとを含んでいる。
【００４１】
“value”を表すフィールドに記載される“１”は、アサーション記述が有効とされた状態であることを示す。“value”を表すフィールドに記載される“０”は、アサーション記述が無効とされた状態であることを示す。
【００４２】
また、本実施形態のアサーションベース検証装置１は、アサーションベース検証の予備的な処理において、“value”を表すフィールドを全て“１”の状態にしたアサーション制御情報２７（初期アサーション制御情報）を生成する。アサーション制御情報２７は、複数のテストパターン２４の各々に対応して用意され、論理シミュレーション時に使用される。
【００４３】
図５は、本実施形態の制御可アサーション記述ファイル２５の構成を例示する図である。図５に示されているように、制御可アサーション記述ファイル２５は、制御用文字列
“//ast_cont_reg[0]//”
が記載されている。その制御用文字列は、assert文の上の行に記載されている。本実施形態の制御可アサーション記述ファイル２５において、そのassert文は、“：”の前にアサーション識別子を備えている。制御可アサーション記述ファイル２５のassert文を、コメント行として処理することで、アサーションベース検証を実行する際に、そのアサーション記述に関連する処理をスキップすることができる。
【００４４】
図６は、本実施形態のアサーションベース検証装置１における前処置（アサーションベース検証を行う前の段階において実行される処理）の動作を概念的に例示するブロック図である。本実施形態のアサーションベース検証装置１において、情報処理装置２のＣＰＵ５は、前処理用プログラム１１を読み出し、その前処理用プログラム１１に示される手順に従って前処理を実行することで、制御可アサーション記述ファイル２５と、アサーション制御情報２７と、発火情報レジスタ２８とを予め生成する。
【００４５】
図６に示されているように、その前処理において、アサーションベース検証装置１はアサーション記述抽出部１４によって、ＤＵＴ（ＲＴＬ）２２からアサーション記述ファイル２１を抽出する。なお、アサーション記述ファイル２１が別ファイルとして用意されている場合には、アサーション記述抽出部１４による抽出処理を省略しても良い。アサーション制御情報生成部１２は、そのアサーション記述ファイル２１を参照して、制御可アサーション記述ファイル２５と、アサーション制御情報２７を生成する。また、発火情報レジスタ生成部１３は、アサーション記述ファイル２１を参照して発火情報レジスタ２８を生成する。
【００４６】
本実施形態のアサーションベース検証装置１は、検証に初期段階で、前処理によって制御可アサーション記述ファイル２５と、アサーション制御情報２７と、発火情報レジスタ２８とを行っている。その後、アサーションベース検証を実行したときに、ＤＵＴ不具合により、ＲＴＬの修正が行われた場合でであっても、従来技術のようにＲＴＬから有限状態機械を再作成する処理を行う必要が無い。本実施形態のアサーションベース検証装置１は、アサーション記述ファイル２１に変更が無い限り、上述の前処理を再実行する必要が無い。
【００４７】
図７は、本実施形態のアサーションベース検証装置１におけるアサーションベース検証（アサーション記述に対応した論理シミュレーション）の動作を概念的に例示するブロック図である。本実施形態のアサーションベース検証装置１において、情報処理装置２のＣＰＵ５が、アサーションベース検証プログラム１５を読み出し、アサーションベース検証プログラム１５に示される手順に従って動作することで、アサーションベース検証装置としての機能を提供する。なお、以下の説明において、上述の前処理は、既に実行されたものとする。
【００４８】
アサーションベース検証を実行する場合、図７に示されているように、アサーションベース検証装置１は、コメント制御アサーション生成部１６として機能し、予め備えられたアサーション制御情報２７と、制御可アサーション記述ファイル２５と読み出す。コメント制御アサーション生成部１６は、アサーション制御情報２７の“value”に対応するフィールドのデータに基づいて、コメント制御アサーション記述ファイル２９を生成する。
【００４９】
コメント制御アサーション記述ファイル２９は、上述の図５に例示された制御可アサーション記述ファイル２５の制御用文字列
“//ast_cont_reg[0]//”
の、下の行をコメント行にすることによって生成される。コメント制御アサーション生成部１６は、アサーション制御情報２７の“value”の値を参照して、“０”が記載されていれば、制御可アサーション記述ファイル２５の対応するassert文を無効にし、“１”が記載されていれば、制御可アサーション記述ファイル２５の対応するassert文を有効にしてコメント制御アサーション記述ファイル２９とする。初回のアサーションベース検証の場合、読み出されたアサーション制御情報２７（初期アサーション制御情報）の各レコードの“value”に対応したフィールドは、全て“１”が記載されている。コメント制御アサーション生成部１６は、その初期アサーション制御情報に基づいて、制御可アサーション記述ファイル２５のassert文を全て有効状態にして、最初のアサーションベース検証用のコメント制御アサーション記述ファイル２９を生成する。
【００５０】
その後、アサーションベース検証装置１は、論理シミュレーション実行部１７として機能し、シミュレーションに用いるテストパターン２４を特定し、コメント制御アサーション記述ファイル２９に対応した論理シミュレーションを行う。このとき、論理シミュレーション実行部１７は、ＤＵＴ（ＲＴＬ）２２、テストベンチ２３、テストパターン２４、および発火情報レジスタ２８を読み出す。また、論理シミュレーション実行部１７は、コメント制御アサーション記述ファイル２９を読み出す。
【００５１】
論理シミュレーション実行部１７は、論理シミュレーションを実行しているときに、コメント制御アサーション記述ファイル２９に含まれるアサーション記述の発火条件と同等な論理である発火情報レジスタ２８のif節を満足するか否かを判断する。このとき、論理シミュレーション実行部１７は、コメント制御アサーション記述ファイル２９に含まれるアサーション記述が、有効か無効かに依存することなく、全ての記述の発火条件と同等な論理である発火情報レジスタ２８のif節を満足するか否かを判断する。論理シミュレーション実行部１７は、その判断の結果に基づいて、条件を満足したif節に対応する発火情報レジスタ２８のレジスタ値を“１”にする。また、論理シミュレーション実行部１７は、与えられた条件を満足しなかった発火条件に対応する発火情報レジスタ２８に対しては何も処理をしないため、初期値“ｘ（不定）”のままである。発火情報レジスタ２８が、Verilog（ヴェリログ）などのハードウェア記述言語を用いて構成されているため、論理シミュレーション実行部１７は、発火情報レジスタ２８のif節の成立／不成立を高速に判定することが可能である。
【００５２】
論理シミュレーション実行部１７は、論理シミュレーションを実行した実行結果を、実行ログ３２として出力する。また、論理シミュレーション実行部１７は、論理シミュレーションが終了した後、発火情報レジスタ２８の値に基づいて、アサーション制御情報２７と同じファイルフォーマットの発火結果ログ３１を生成する。このとき、発火情報レジスタ２８の値が、“ｘ（不定）”である場合は、“０”に置き換えて発火結果ログ３１を生成する。論理シミュレーション実行部１７は、発火結果ログ３１をそのまま、アサーション制御情報２７として更新する。更新されたアサーション制御情報２７は、次回のアサーションベース検証に使用される。
【００５３】
実行ログ３２にアサーションエラー情報が含まれるとき、ＤＵＴ（ＲＴＬ）２２は、そのアサーションエラー情報に対応して、ＤＵＴ（ＲＴＬ）２２の解析や不具合修正が施される。アサーションベース検証装置１は、上述の発火結果ログ３１を新たなアサーション制御情報２７として用いて、修正されたＤＵＴ（ＲＴＬ）２２に対応するアサーションベース検証を実行する。
【００５４】
２回目（若しくはそれ以降）のアサーションベース検証を実行する場合、“value”に対応したフィールドに、“０”が記載されているレコードを含むアサーション制御情報２７が用いられる。コメント制御アサーション生成部１６は、そのアサーション制御情報２７に基づいて、新たなコメント制御アサーション記述ファイル２９を生成する。論理シミュレーション実行部１７は、２回目の以降のアサーションベース検証において、検証の対象外とされたアサーション記述をスキップして、アサーションベース検証に対応した論理シミュレーションを実行する。
【００５５】
このとき、論理シミュレーション実行部１７は、発火情報レジスタ２８によって、全ての発火条件に対し、その条件の成立／不成立に関する情報を記憶する。発火情報レジスタ２８が、全ての発火条件に関する情報を記憶しているので、修正されたＤＵＴ（ＲＴＬ）２２に対する検証の結果、前回の論理シミュレーションでは、条件が成立しなかった発火条件が、今回の論理シミュレーションで成立した場合、その情報は、今回出力される発火情報レジスタ２８に記憶される。
【００５６】
アサーションベース検証装置１は、論理シミュレーション実行部１７による論理シミュレーションが終了した後、差分ログ生成部１８として機能する。差分ログ生成部１８は、発火結果ログ３１と、アサーション制御情報２７とを読み出し、それらの差分を抽出する処理を行う。差分ログ生成部１８によって、発火結果ログ３１とアサーション制御情報２７との差分を抽出し、差分ログ３３を生成することで、ユーザーは、不具合を修正したことによって、新たな動作の変化を迅速に把握することができる。
【００５７】
例えば、２回目の論理シミュレーションで発火情報レジスタ２８が更新された場合、その発火情報レジスタ２８に対応した発火結果ログ３１が出力される。その発火結果ログ３１と、入力に用いたアサーション制御情報２７とを比較することで、無効にされていたアサーションが、実際には有効にすべきであるか否かの判断を行うことが可能となる。
【００５８】
また、発火結果ログ３１とアサーション制御情報２７とに差分がない場合や、無効であったアサーション記述に対し、ユーザーが手動で有効にした箇所のみが差分として記録される場合には、アサーションエラー情報に対応した不具合の修正後においても、新たに有効にすべきアサーションはなかった、つまり十分なアサーション記述を用いて論理シミュレーションを行ったと判断することが可能である。
【００５９】
しかし、それ以外の差分が生じている場合には、アサーションエラー情報に対応して不具合を修正したことにより、修正箇所以外の動作が変化していたり、同じテストパタンでも、前回と異なるタイミングで動作していたりする可能性がある。ユーザーは、差分ログ３３を参照することによって、そのような状況を迅速に発見することが可能となる。
【００６０】
本実施形態のアサーションベース検証装置１において、アサーション制御情報２７は、複数のテストパターン２４の各々に対応して用意されていることが好ましい。アサーション制御情報２７は、上述の前処理によって、各テストパターン分のアサーション制御情報２７が生成される。１回目のアサーションベース検証を行う場合には、使用するテストパターンに対応した初期状態のアサーション制御情報２７を特定して使用する。２回目以降のアサーションベース検証では、発火結果ログ３１に基づいた新たなアサーション制御情報２７を使用することで、発火条件が成立するアサーション記述のみを検証の対象とし、検証の対象外のアサーション記述をスキップすることができる。
【００６１】
なお、アサーション制御情報２７は、ユーザーが手動で有効／無効の情報を変更することが可能である。例えば、機能単位で有効にしたい場合や、特定のアサーション記述を常時有効に設定しておきたい場合などに、対応するアサーション記述に対し、アサーション制御情報２７の“value”の設定を個別に変更・修正してもよい。
【００６２】
また、複数のテストパターン２４の全ての発火結果ログ３１の総和を取ることで、一度も条件の成立がなかった発火条件を含むアサーション記述を見つけることができる。ユーザーは、一度も条件の成立がなかった発火条件を含むアサーション記述が見つかった場合、そのアサーション記述が、不要なアサーション記述であるのか、記述に間違いがあるアサーション記述なのかなどの判断を行うことができる。その判断の結果、不要なアサーション記述ならば削除し、記述の間違いであるならば修正することで、ＴＡＴを短縮しつつ品質の向上に務めることができる。
【００６３】
本実施形態のアサーションベース検証装置１による実行ＴＡＴの削減は、大規模回路やチップ全体のシミュレーションなどで、対象となるアサーション記述が多い場合に、より大きな効果を奏することができる。また、テストパターンに依存して、動作していない回路部分が大きい場合にも、より大きな効果を奏することができる。
【００６４】
［第２実施形態］
以下に、図面を参照して本願発明のアサーションベース検証装置１の第２実施形態について説明を行う。第２実施形態のアサーションベース検証装置１は、論理シミュレーションを実行する前に、制御可アサーション記述ファイル２５を生成する。その制御可アサーション記述ファイル２５は、アサーション記述ファイル２１のプロパティ記述のdisable iff節の条件文に対して、評価無効とするための条件を追加する処理をすることで生成される。それによって、第２実施形態のアサーションベース検証装置１は、コメント制御アサーション生成部１６によって生成されるコメント制御アサーション記述ファイル２９を用いることなく、アサーション記述の有効／無効を制御する。
【００６５】
図８は、第２実施形態の制御可アサーション記述ファイル２５の構成を例示する図である。第２実施形態の制御可アサーション記述ファイル２５は、アサーション制御情報生成部１２によって、アサーション記述ファイル２１の
“property”
と
“endproperty”
とで囲まれたプロパティ記述のdisable iff節の条件に、アサーション制御情報２７の“value”の値を格納したレジスタast_cont_reg[0:AST_NUM-1]の対応する１ビットを追加した形で生成される。また、同時に、ast_cont_reg[0:AST_NUM-1]というレジスタ、及び、論理シミュレーション開始時にアサーション制御情報２７の“value”の値をこのレジスタにロードするテストベンチ記述が生成される。これによって、論理シミュレーション実行時に、アサーション制御情報２７の値を格納するレジスタ
ast_cont_reg[0:AST_NUM-1]
にアサーション制御情報２７をロードするだけで、制御可アサーション記述ファイル２５のアサーション記述の有効／無効を制御することができる。図８に示されているように、制御可アサーション記述ファイル２５の、disable iff節の“（!rst_n|!ast_cont_reg[0]）”の内部が真であれば、処理は終了する。具体的には、ast_cont_reg[0]の値が０であるならば処理は終了する。
【００６６】
図９は、第２実施形態のアサーションベース検証装置１におけるアサーションベース検証（アサーション記述に対応した論理シミュレーション）の動作を概念的に例示するブロック図である。第２実施形態のアサーションベース検証装置１は、コメント制御アサーション生成部１６として機能することなく処理を行う。図９に示されているように、アサーションベース検証装置１は、論理シミュレーション実行部１７として機能し、制御可アサーション記述ファイル２５と、アサーション制御情報２７と、テストベンチ２３と、テストパターン２４と、ＤＵＴ（ＲＴＬ）２２と、発火情報レジスタ２８とを読み出す。
【００６７】
第２実施形態のアサーションベース検証装置１における論理シミュレーション実行部１７は、シミュレーションに用いるテストパターン２４を特定し、disable iff節に条件が追加された制御可アサーション記述ファイル２５に対応した論理シミュレーションを行う。このとき、論理シミュレーション実行部１７は、ＤＵＴ（ＲＴＬ）２２、テストベンチ２３、テストパターン２４、および発火情報レジスタ２８を読み出す。また、論理シミュレーション実行部１７は、アサーション制御情報２７と制御可アサーション記述ファイル２５を読み出す。このとき、論理シミュレーション実行部１７は、そのアサーション制御情報２７の値を用いて、制御可アサーション記述ファイル２５のdisable iff節の、“（!rst_n|!ast_cont_reg[0]）”の内部が真となるアサーション記述を評価無効として、アサーション記述に対応した論理シミュレーションを実行する。これによって、第１実施形態のような、無効にされたassert文を含むコメント制御アサーション記述ファイル２９を使用した場合と同様に、アサーションベース検証を実行する際に、評価無効のアサーション記述に関連する処理をスキップすることができる。その後、アサーション記述に対応した論理シミュレーションを実行した結果として、発火結果ログ３１、実行ログ３２、差分ログ３３を生成する。
【００６８】
第２実施形態のアサーションベース検証装置１は、コメント制御アサーション記述ファイル２９を生成するための処理を行うことなく、アサーションベース検証を実現している。これによって、品質を低下させることなくシミュレーションの実行ＴＡＴを短縮することが可能である。
【００６９】
以上、本願発明の実施の形態を具体的に説明した。本願発明は上述の実施の形態に限定されるものではなく、その要旨を逸脱しない範囲で種々変更可能である。また、上述の複数の実施形態は、その構成・動作に矛盾が生じない範囲において組み合わせて実施することが可能である。
【符号の説明】
【００７０】
１…アサーションベース検証装置
２…情報処理装置
３…入力装置
４…出力装置
５…ＣＰＵ
６…メモリ
７…入出力インターフェース
８…大容量記憶装置
９…バス
１１…前処理用プログラム
１２…アサーション制御情報生成部
１３…発火情報レジスタ生成部
１４…アサーション記述抽出部
１５…アサーションベース検証プログラム
１６…コメント制御アサーション生成部
１７…論理シミュレーション実行部
１８…差分ログ生成部
２１…アサーション記述ファイル
２２…ＤＵＴ（ＲＴＬ）
２３…テストベンチ
２４…テストパターン
２５…制御可アサーション記述ファイル
２７…アサーション制御情報
２８…発火情報レジスタ
２９…コメント制御アサーション記述ファイル
３１…発火結果ログ
３２…実行ログ
３３…差分ログ
【特許請求の範囲】
【請求項１】
アサーションベース検証用の情報を記憶する記憶部と、
アサーションベース検証に対応した論理シミュレーションを実行する論理シミュレーション実行部としての機能を提供する演算処理部と、
を具備し、
前記記憶部は、
前記論理シミュレーションの対象であるＤＵＴと、
前記アサーションベース検証で使用されるアサーション記述に含まれる発火条件と、前記発火条件を満足したか否かに関する情報とを関連付けて記憶する発火情報レジスタと、
アサーション記述を処理対象とするか否かの設定が可能な制御可アサーション記述ファイルと、
前記制御可アサーション記述ファイルの前記設定を制御するためのアサーション制御情報と
を記憶し、
前記演算処理部は、
前記論理シミュレーション実行部の機能によって、
前記制御可アサーション記述ファイルのアサーション記述のうち、前記アサーション制御情報によって処理対象に指定されたアサーション記述を、処理対象アサーション記述とし、前記アサーション制御情報によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述として特定し、
前記処理対象アサーション記述を用いて前記ＤＵＴに対するアサーションベース検証を実行した結果を実行ログに記録し、
前記発火条件を満足したか否かを判定した結果に基づいて前記発火情報レジスタを書き換え、前記発火情報レジスタのデータに基づいて発火結果ログを生成し、
前記発火結果ログに基づいて前記アサーション制御情報を更新して新たなアサーション制御情報とし、前記新たなアサーション制御情報を用いて前記アサーションベース検証を実行する
アサーションベース検証装置。
【請求項２】
請求項１に記載のアサーションベース検証装置において、
前記実行ログに含まれるエラー情報に応じて前記ＤＵＴが修正されて新たなＤＵＴとして供給されたとき、
前記論理シミュレーション実行部は、
前記新たなアサーション制御情報を用いて前記新たなＤＵＴに対する前記アサーションベース検証を実行する
アサーションベース検証装置。
【請求項３】
請求項１または２に記載のアサーションベース検証装置において、さらに、
差分ログ生成部を具備し、
前記差分ログ生成部は、
前記発火結果ログと、前記アサーション制御情報とを読み出し、
前記アサーション制御情報によって処理対象とされたアサーション記述と、前記発火結果ログに条件を満足していることが記録されている発火条件に対応するアサーション記述との比較に基づいて差分ログを生成する
アサーションベース検証装置。
【請求項４】
請求項１から３のいずれか１項に記載のアサーションベース検証装置において、
前記記憶部は、
全てのアサーション記述を有効に設定した初期状態のアサーション制御情報を予め記憶し、
前記論理シミュレーション実行部は、
アサーションベース検証の開始に応じて、前記初期状態のアサーション制御情報に基づいて、前記制御可アサーション記述ファイルの全てのアサーション記述を処理対象アサーション記述として初回のアサーションベース検証を実行し、
前記初回のアサーションベース検証の終了時に、初回実行ログと初回発火結果ログとを生成し、
前記初回実行ログと前記初回発火結果ログと基づいて次回のアサーションベース検証を実行する
アサーションベース検証装置。
【請求項５】
請求項１から４のいずれか１項に記載のアサーションベース検証装置において、
前記発火情報レジスタは、
ハードウェア記述言語を用いて表現され、
複数の発火条件と、前記複数の発火条件の各々を満足したか否かに関する情報とを一対一に関連付けて記憶する
アサーションベース検証装置。
【請求項６】
請求項１から５のいずれか１項に記載のアサーションベース検証装置において、さらに、
コメント制御アサーション生成部を具備し、
前記制御可アサーション記述ファイルは、
アサーション命令の前に追加された制御文字を有し、
前記コメント制御アサーション生成部は、
前記制御文字に基づいて、前記処理対象アサーション記述と、前記処理非対象アサーション記述とを有するコメント制御アサーション記述ファイルを生成し、
前記論理シミュレーション実行部は、
前記コメント制御アサーション記述ファイルで処理対象とされたアサーション記述を用いてアサーションベース検証を実行する
アサーションベース検証装置。
【請求項７】
請求項１から５のいずれか１項に記載のアサーションベース検証装置において、
前記制御可アサーション記述ファイルは、
アサーション記述の内部に記述された評価有効／無効判定節の条件文を有し、
前記論理シミュレーション実行部は、
前記評価有効／無効判定節の条件文に基づいて、前記アサーション制御情報によって処理対象に指定されたアサーション記述を処理対象アサーション記述とし、前記アサーション制御情報によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述と同等なものとして特定する
アサーションベース検証装置。
【請求項８】
請求項１から７のいずれか１項に記載のアサーションベース検証装置において、さらに、
前記アサーションベース検証の準備として実行される前処理を行う前処理部を具備し、
前記前処理部は、
初期状態のアサーション制御情報を生成するアサーション制御情報生成部と、
初期状態の発火情報レジスタを生成する発火情報レジスタ生成部と
を備え、
前記アサーション制御情報生成部は、
複数のアサーション記述の各々を特定するためのアサーション名と、前記アサーション名に対応するアサーション記述の有効／無効を示す情報とを対応付けて前記アサーション制御情報を生成し、
前記発火情報レジスタ生成部は、
前記複数のアサーション記述の各々の発火条件と、前記発火条件の成立／不成立を示す情報とを対応付けて前記発火情報レジスタを生成する
アサーションベース検証装置。
【請求項９】
請求項８に記載のアサーションベース検証装置において、
前記前処理部は、さらに、
アサーション記述抽出部を備え、
前記アサーション記述抽出部は、
前記ＤＵＴに含まれるアサーション記述を抽出して前記アサーション記述ファイルを生成する
アサーションベース検証装置。
【請求項１０】
（ａ）アサーションベース検証用の情報を読み出すステップと、
（ｂ）前記アサーションベース検証用の情報に基づいてアサーションベース検証に対応した論理シミュレーションを実行するステップと
を具備し、
前記（ａ）ステップは、
論理シミュレーションの対象であるＤＵＴを読み出すステップと、
前記アサーションベース検証で使用されるアサーション記述に含まれる発火条件と、前記発火条件を満足したか否かに関する情報とを関連付けて記憶する発火情報レジスタを読み出すステップと、
アサーション記述を処理対象とするか否かの設定が可能な制御可アサーション記述ファイルを読み出すステップと、
前記制御可アサーション記述ファイルの前記設定を制御するためのアサーション制御情報を読み出すステップと
を備え、
前記（ｂ）ステップは、
前記制御可アサーション記述ファイルのアサーション記述のうち、前記アサーション制御情報によって処理対象に指定されたアサーション記述を、処理対象アサーション記述とし、前記アサーション制御情報によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述として特定する有効記述特定ステップと、
前記処理対象アサーション記述を用いて前記ＤＵＴに対するアサーションベース検証を実行した結果を実行ログに記録する実行ログ生成ステップと、
前記発火条件を満足したか否かを判定した結果に基づいて前記発火情報レジスタを書き換え、前記発火情報レジスタのデータに基づいて発火結果ログを生成する発火結果ログ生成ステップと、
前記発火結果ログに基づいて前記アサーション制御情報を更新して新たなアサーション制御情報とし、前記新たなアサーション制御情報を用いて前記アサーションベース検証を実行するアサーションベース検証ステップと
を備える
アサーションベース検証方法。
【請求項１１】
請求項１０に記載のアサーションベース検証方法において、
前記実行ログに含まれるエラー情報に応じて前記ＤＵＴが修正されて新たなＤＵＴとして供給されたとき、
前記（ｂ）ステップは、
前記新たなアサーション制御情報を用いて前記新たなＤＵＴに対する前記アサーションベース検証を実行するステップ
を具備する
アサーションベース検証方法。
【請求項１２】
請求項１０または１１に記載のアサーションベース検証方法において、
前記（ｂ）ステップは、
前記発火結果ログと、前記アサーション制御情報とを読み出し、前記アサーション制御情報によって処理対象とされたアサーション記述と、前記発火結果ログに条件を満足していることが記録されている発火条件に対応するアサーション記述との比較に基づいて差分ログを生成するステップ
を備える
アサーションベース検証方法。
【請求項１３】
請求項１０から１２のいずれか１項に記載のアサーションベース検証方法において、
前記（ａ）ステップは、
予め記憶された、全てのアサーション記述を有効に設定した初期状態のアサーション制御情報を読み出すステップを含み、
前記（ｂ）ステップは、
アサーションベース検証の開始に応じて、前記初期状態のアサーション制御情報に基づいて、前記制御可アサーション記述ファイルの全てのアサーション記述を処理対象アサーション記述として初回のアサーションベース検証を実行するステップと、
前記初回のアサーションベース検証の終了時に、初回実行ログと初回発火結果ログとを生成するステップと、
前記初回実行ログと前記初回発火結果ログと基づいて次回のアサーションベース検証を実行するステップと
を備える
アサーションベース検証方法。
【請求項１４】
請求項１０から１３のいずれか１項に記載のアサーションベース検証方法において、
前記発火情報レジスタは、ハードウェア記述言語を用いて表現され、
複数の発火条件と、前記複数の発火条件の各々を満足したか否かに関する情報とを一対一に関連付けて記憶する
アサーションベース検証方法。
【請求項１５】
請求項１０から１４のいずれか１項に記載のアサーションベース検証方法において、
前記制御可アサーション記述ファイルは、
アサーション命令の前に追加された制御文字を有し、
前記（ｂ）ステップは、
前記制御文字に基づいて、前記処理対象アサーション記述と、前記処理非対象アサーション記述とを有するコメント制御アサーション記述ファイルを生成するステップと、
前記コメント制御アサーション記述ファイルで処理対象とされたアサーション記述を用いてアサーションベース検証を実行するステップと
を備える
アサーションベース検証方法。
【請求項１６】
請求項１０から１４のいずれか１項に記載のアサーションベース検証方法において、
前記制御可アサーション記述ファイルは、
アサーション記述の内部に記述された評価有効／無効判定節の条件文を有し、
前記（ｂ）ステップは、
前記評価有効／無効判定節の条件文に基づいて、前記アサーション制御情報によって処理対象に指定されたアサーション記述を処理対象アサーション記述とし、前記アサーション制御情報によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述と同等なものとして特定するステップ
を備える
アサーションベース検証方法。
【請求項１７】
請求項１０から１６のいずれか１項に記載のアサーションベース検証方法において、さらに、
（ｃ）前記アサーションベース検証の準備として前処理を行うステップを具備し、
前記（ｃ）ステップは、
複数のアサーション記述の各々を特定するためのアサーション名と、前記アサーション名に対応するアサーション記述の有効／無効を示す情報とを対応付けて前記アサーション制御情報を生成するステップと、
前記複数のアサーション記述の各々の発火条件と、前記発火条件の成立／不成立を示す情報とを対応付けて前記発火情報レジスタを生成するステップと
を備える
アサーションベース検証方法。
【請求項１８】
請求項１７に記載のアサーションベース検証方法において、
前記（ｃ）ステップは、
前記ＤＵＴに含まれるアサーション記述を抽出して前記アサーション記述ファイルを生成するステップを備える
アサーションベース検証方法。
【請求項１】
アサーションベース検証用の情報を記憶する記憶部と、
アサーションベース検証に対応した論理シミュレーションを実行する論理シミュレーション実行部としての機能を提供する演算処理部と、
を具備し、
前記記憶部は、
前記論理シミュレーションの対象であるＤＵＴと、
前記アサーションベース検証で使用されるアサーション記述に含まれる発火条件と、前記発火条件を満足したか否かに関する情報とを関連付けて記憶する発火情報レジスタと、
アサーション記述を処理対象とするか否かの設定が可能な制御可アサーション記述ファイルと、
前記制御可アサーション記述ファイルの前記設定を制御するためのアサーション制御情報と
を記憶し、
前記演算処理部は、
前記論理シミュレーション実行部の機能によって、
前記制御可アサーション記述ファイルのアサーション記述のうち、前記アサーション制御情報によって処理対象に指定されたアサーション記述を、処理対象アサーション記述とし、前記アサーション制御情報によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述として特定し、
前記処理対象アサーション記述を用いて前記ＤＵＴに対するアサーションベース検証を実行した結果を実行ログに記録し、
前記発火条件を満足したか否かを判定した結果に基づいて前記発火情報レジスタを書き換え、前記発火情報レジスタのデータに基づいて発火結果ログを生成し、
前記発火結果ログに基づいて前記アサーション制御情報を更新して新たなアサーション制御情報とし、前記新たなアサーション制御情報を用いて前記アサーションベース検証を実行する
アサーションベース検証装置。
【請求項２】
請求項１に記載のアサーションベース検証装置において、
前記実行ログに含まれるエラー情報に応じて前記ＤＵＴが修正されて新たなＤＵＴとして供給されたとき、
前記論理シミュレーション実行部は、
前記新たなアサーション制御情報を用いて前記新たなＤＵＴに対する前記アサーションベース検証を実行する
アサーションベース検証装置。
【請求項３】
請求項１または２に記載のアサーションベース検証装置において、さらに、
差分ログ生成部を具備し、
前記差分ログ生成部は、
前記発火結果ログと、前記アサーション制御情報とを読み出し、
前記アサーション制御情報によって処理対象とされたアサーション記述と、前記発火結果ログに条件を満足していることが記録されている発火条件に対応するアサーション記述との比較に基づいて差分ログを生成する
アサーションベース検証装置。
【請求項４】
請求項１から３のいずれか１項に記載のアサーションベース検証装置において、
前記記憶部は、
全てのアサーション記述を有効に設定した初期状態のアサーション制御情報を予め記憶し、
前記論理シミュレーション実行部は、
アサーションベース検証の開始に応じて、前記初期状態のアサーション制御情報に基づいて、前記制御可アサーション記述ファイルの全てのアサーション記述を処理対象アサーション記述として初回のアサーションベース検証を実行し、
前記初回のアサーションベース検証の終了時に、初回実行ログと初回発火結果ログとを生成し、
前記初回実行ログと前記初回発火結果ログと基づいて次回のアサーションベース検証を実行する
アサーションベース検証装置。
【請求項５】
請求項１から４のいずれか１項に記載のアサーションベース検証装置において、
前記発火情報レジスタは、
ハードウェア記述言語を用いて表現され、
複数の発火条件と、前記複数の発火条件の各々を満足したか否かに関する情報とを一対一に関連付けて記憶する
アサーションベース検証装置。
【請求項６】
請求項１から５のいずれか１項に記載のアサーションベース検証装置において、さらに、
コメント制御アサーション生成部を具備し、
前記制御可アサーション記述ファイルは、
アサーション命令の前に追加された制御文字を有し、
前記コメント制御アサーション生成部は、
前記制御文字に基づいて、前記処理対象アサーション記述と、前記処理非対象アサーション記述とを有するコメント制御アサーション記述ファイルを生成し、
前記論理シミュレーション実行部は、
前記コメント制御アサーション記述ファイルで処理対象とされたアサーション記述を用いてアサーションベース検証を実行する
アサーションベース検証装置。
【請求項７】
請求項１から５のいずれか１項に記載のアサーションベース検証装置において、
前記制御可アサーション記述ファイルは、
アサーション記述の内部に記述された評価有効／無効判定節の条件文を有し、
前記論理シミュレーション実行部は、
前記評価有効／無効判定節の条件文に基づいて、前記アサーション制御情報によって処理対象に指定されたアサーション記述を処理対象アサーション記述とし、前記アサーション制御情報によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述と同等なものとして特定する
アサーションベース検証装置。
【請求項８】
請求項１から７のいずれか１項に記載のアサーションベース検証装置において、さらに、
前記アサーションベース検証の準備として実行される前処理を行う前処理部を具備し、
前記前処理部は、
初期状態のアサーション制御情報を生成するアサーション制御情報生成部と、
初期状態の発火情報レジスタを生成する発火情報レジスタ生成部と
を備え、
前記アサーション制御情報生成部は、
複数のアサーション記述の各々を特定するためのアサーション名と、前記アサーション名に対応するアサーション記述の有効／無効を示す情報とを対応付けて前記アサーション制御情報を生成し、
前記発火情報レジスタ生成部は、
前記複数のアサーション記述の各々の発火条件と、前記発火条件の成立／不成立を示す情報とを対応付けて前記発火情報レジスタを生成する
アサーションベース検証装置。
【請求項９】
請求項８に記載のアサーションベース検証装置において、
前記前処理部は、さらに、
アサーション記述抽出部を備え、
前記アサーション記述抽出部は、
前記ＤＵＴに含まれるアサーション記述を抽出して前記アサーション記述ファイルを生成する
アサーションベース検証装置。
【請求項１０】
（ａ）アサーションベース検証用の情報を読み出すステップと、
（ｂ）前記アサーションベース検証用の情報に基づいてアサーションベース検証に対応した論理シミュレーションを実行するステップと
を具備し、
前記（ａ）ステップは、
論理シミュレーションの対象であるＤＵＴを読み出すステップと、
前記アサーションベース検証で使用されるアサーション記述に含まれる発火条件と、前記発火条件を満足したか否かに関する情報とを関連付けて記憶する発火情報レジスタを読み出すステップと、
アサーション記述を処理対象とするか否かの設定が可能な制御可アサーション記述ファイルを読み出すステップと、
前記制御可アサーション記述ファイルの前記設定を制御するためのアサーション制御情報を読み出すステップと
を備え、
前記（ｂ）ステップは、
前記制御可アサーション記述ファイルのアサーション記述のうち、前記アサーション制御情報によって処理対象に指定されたアサーション記述を、処理対象アサーション記述とし、前記アサーション制御情報によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述として特定する有効記述特定ステップと、
前記処理対象アサーション記述を用いて前記ＤＵＴに対するアサーションベース検証を実行した結果を実行ログに記録する実行ログ生成ステップと、
前記発火条件を満足したか否かを判定した結果に基づいて前記発火情報レジスタを書き換え、前記発火情報レジスタのデータに基づいて発火結果ログを生成する発火結果ログ生成ステップと、
前記発火結果ログに基づいて前記アサーション制御情報を更新して新たなアサーション制御情報とし、前記新たなアサーション制御情報を用いて前記アサーションベース検証を実行するアサーションベース検証ステップと
を備える
アサーションベース検証方法。
【請求項１１】
請求項１０に記載のアサーションベース検証方法において、
前記実行ログに含まれるエラー情報に応じて前記ＤＵＴが修正されて新たなＤＵＴとして供給されたとき、
前記（ｂ）ステップは、
前記新たなアサーション制御情報を用いて前記新たなＤＵＴに対する前記アサーションベース検証を実行するステップ
を具備する
アサーションベース検証方法。
【請求項１２】
請求項１０または１１に記載のアサーションベース検証方法において、
前記（ｂ）ステップは、
前記発火結果ログと、前記アサーション制御情報とを読み出し、前記アサーション制御情報によって処理対象とされたアサーション記述と、前記発火結果ログに条件を満足していることが記録されている発火条件に対応するアサーション記述との比較に基づいて差分ログを生成するステップ
を備える
アサーションベース検証方法。
【請求項１３】
請求項１０から１２のいずれか１項に記載のアサーションベース検証方法において、
前記（ａ）ステップは、
予め記憶された、全てのアサーション記述を有効に設定した初期状態のアサーション制御情報を読み出すステップを含み、
前記（ｂ）ステップは、
アサーションベース検証の開始に応じて、前記初期状態のアサーション制御情報に基づいて、前記制御可アサーション記述ファイルの全てのアサーション記述を処理対象アサーション記述として初回のアサーションベース検証を実行するステップと、
前記初回のアサーションベース検証の終了時に、初回実行ログと初回発火結果ログとを生成するステップと、
前記初回実行ログと前記初回発火結果ログと基づいて次回のアサーションベース検証を実行するステップと
を備える
アサーションベース検証方法。
【請求項１４】
請求項１０から１３のいずれか１項に記載のアサーションベース検証方法において、
前記発火情報レジスタは、ハードウェア記述言語を用いて表現され、
複数の発火条件と、前記複数の発火条件の各々を満足したか否かに関する情報とを一対一に関連付けて記憶する
アサーションベース検証方法。
【請求項１５】
請求項１０から１４のいずれか１項に記載のアサーションベース検証方法において、
前記制御可アサーション記述ファイルは、
アサーション命令の前に追加された制御文字を有し、
前記（ｂ）ステップは、
前記制御文字に基づいて、前記処理対象アサーション記述と、前記処理非対象アサーション記述とを有するコメント制御アサーション記述ファイルを生成するステップと、
前記コメント制御アサーション記述ファイルで処理対象とされたアサーション記述を用いてアサーションベース検証を実行するステップと
を備える
アサーションベース検証方法。
【請求項１６】
請求項１０から１４のいずれか１項に記載のアサーションベース検証方法において、
前記制御可アサーション記述ファイルは、
アサーション記述の内部に記述された評価有効／無効判定節の条件文を有し、
前記（ｂ）ステップは、
前記評価有効／無効判定節の条件文に基づいて、前記アサーション制御情報によって処理対象に指定されたアサーション記述を処理対象アサーション記述とし、前記アサーション制御情報によって処理対象に指定されていないアサーション記述を、処理非対象アサーション記述と同等なものとして特定するステップ
を備える
アサーションベース検証方法。
【請求項１７】
請求項１０から１６のいずれか１項に記載のアサーションベース検証方法において、さらに、
（ｃ）前記アサーションベース検証の準備として前処理を行うステップを具備し、
前記（ｃ）ステップは、
複数のアサーション記述の各々を特定するためのアサーション名と、前記アサーション名に対応するアサーション記述の有効／無効を示す情報とを対応付けて前記アサーション制御情報を生成するステップと、
前記複数のアサーション記述の各々の発火条件と、前記発火条件の成立／不成立を示す情報とを対応付けて前記発火情報レジスタを生成するステップと
を備える
アサーションベース検証方法。
【請求項１８】
請求項１７に記載のアサーションベース検証方法において、
前記（ｃ）ステップは、
前記ＤＵＴに含まれるアサーション記述を抽出して前記アサーション記述ファイルを生成するステップを備える
アサーションベース検証方法。
【図１】
【図２Ａ】
【図２Ｂ】
【図３Ａ】
【図３Ｂ】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図２Ａ】
【図２Ｂ】
【図３Ａ】
【図３Ｂ】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【公開番号】特開２０１１−２５３３１３（Ｐ２０１１−２５３３１３Ａ）
【公開日】平成２３年１２月１５日（２０１１．１２．１５）
【国際特許分類】
【出願番号】特願２０１０−１２６１８８（Ｐ２０１０−１２６１８８）
【出願日】平成２２年６月１日（２０１０．６．１）
【出願人】（３０２０６２９３１）ルネサスエレクトロニクス株式会社 (8,021)
【Ｆターム（参考）】
【公開日】平成２３年１２月１５日（２０１１．１２．１５）
【国際特許分類】
【出願日】平成２２年６月１日（２０１０．６．１）
【出願人】（３０２０６２９３１）ルネサスエレクトロニクス株式会社 (8,021)
【Ｆターム（参考）】
[ Back to top ]