特許ウォッチ

公開番号2025125954
公報種別公開特許公報(A)
公開日2025-08-28
出願番号2024022266
出願日2024-02-16
発明の名称等価性検証装置、等価性検証方法及び等価性検証プログラム
出願人株式会社SCU
代理人個人,個人
主分類G06F 30/3323 20200101AFI20250821BHJP(計算;計数)
要約【課題】組合せ論理回路及び順序回路を含む算術演算回路と設計仕様との等価性検証を効率的に行うことが課題である。
【解決手段】等価性検証装置10は、仕様記述のタイミングチャートに基づいてネットリストにある算術演算回路を動作させた場合に出力される各ビットに対応するブール多項式を、出力のビット毎に生成する。そして等価性検証装置10は、仕様記述に基づいてプライマリ出力の各ビットに対応するブール多項式を、ネットリストに基づいて算出されたブール多項式のブール多項式環を用いて生成する。その後、等価性検証装置10は、ネットリストに基づいて算出したブール多項式と仕様記述に基づいて算出したブール多項式の差を算出し、すべてのビットに対して差が0である場合に、設計されたネットリストは、仕様記述を満たしていると判定する。
【選択図】図1
特許請求の範囲【請求項１】
組合せ論理回路及び順序回路を含む算術演算回路のネットリストと、設計仕様の仕様記述との等価性を計算機代数により検証する等価性検証装置であって、
前記ネットリストと前記仕様記述に含まれるタイミングチャートに基づいて第１のブール多項式を生成する第１の生成手段と、
前記仕様記述に含まれる論理関数に基づいて第２のブール多項式を生成する第２の生成手段と、
前記第１の生成手段により生成された前記第１のブール多項式と、前記第２の生成手段により生成された前記第２のブール多項式の差分を算出する算出手段と、
前記算出手段により算出された差分に基づいて、前記ネットリストと前記仕様記述との等価性を判定する判定手段と
を備えたことを特徴とする等価性検証装置。
続きを表示（約 1,400 文字）【請求項２】
前記第１の生成手段は、
前記タイミングチャートに基づいて前記ネットリストが示す前記算術演算回路を動作させた場合に、前記算術演算回路への複数の入力と該算術演算回路内の前記順序回路からの複数の出力とを変数とした前記第１のブール多項式を生成することを特徴とする請求項１に記載の等価性検証装置。
【請求項３】
前記第１の生成手段は、
前記タイミングチャートのクロックの立ち上がりエッジ直前の前記算術演算回路への複数の入力と、前記立ち上がりエッジ直前の該算術演算回路内の前記順序回路からの複数の出力とを変数とした前記第１のブール多項式を生成することを特徴とする請求項２に記載の等価性検証装置。
【請求項４】
前記判定手段は、
前記算出手段により算出された差分が０である場合に、前記ネットリストと前記仕様記述とが等価であると判定することを特徴とする請求項１に記載の等価性検証装置。
【請求項５】
前記判定手段は、
前記算出手段により算出された差分に、前記順序回路からの複数の出力に対応する変数が含まれていた場合に、前記算術演算回路の内部初期状態に依存する誤り又は不正回路の混入が存在すると判定することを特徴とする請求項１に記載の等価性検証装置。
【請求項６】
前記判定手段は、
前記算出手段により算出された差分に０でないブール多項式が含まれていた場合に、前記算術演算回路の入力のみに依存する誤り又は不正回路の混入が存在すると判定することを特徴とする請求項１に記載の等価性検証装置。
【請求項７】
組合せ論理回路及び順序回路を含む算術演算回路のネットリストと、設計仕様の仕様記述との等価性を計算機代数により検証する等価性検証装置における等価性検証方法であって、
前記ネットリストと前記仕様記述に含まれるタイミングチャートに基づいて第１のブール多項式を生成する第１の生成工程と、
前記仕様記述に含まれる論理関数に基づいて第２のブール多項式を生成する第２の生成工程と、
前記第１の生成工程により生成された前記第１のブール多項式と、前記第２の生成工程により生成された前記第２のブール多項式の差分を算出する算出工程と、
前記算出工程により算出された差分に基づいて、前記ネットリストと前記仕様記述との等価性を判定する判定工程と
を含むことを特徴とする等価性検証方法。
【請求項８】
組合せ論理回路及び順序回路を含む算術演算回路のネットリストと、設計仕様の仕様記述との等価性を計算機代数により検証する等価性検証装置で実行される等価性検証プログラムであって、
前記ネットリストと前記仕様記述に含まれるタイミングチャートに基づいて第１のブール多項式を生成する第１の生成手順と、
前記仕様記述に含まれる論理関数に基づいて第２のブール多項式を生成する第２の生成手順と、
前記第１の生成手順により生成された前記第１のブール多項式と、前記第２の生成手順により生成された前記第２のブール多項式の差分を算出する算出手順と、
前記算出手順により算出された差分に基づいて、前記ネットリストと前記仕様記述との等価性を判定する判定手順と
をコンピュータに実行させることを特徴とする等価性検証プログラム。

発明の詳細な説明【技術分野】
【０００１】
本発明は、組合せ論理回路及び順序回路を含む算術演算回路と設計仕様との等価性検証を効率的に行うことができる等価性検証装置、等価性検証方法及び等価性検証プログラムに関する。
続きを表示（約 2,500 文字）【背景技術】
【０００２】
従来、ガロア体上の乗算などの算術演算を含む回路（以下、「算術演算回路」と言う）が、あらかじめ定められた設計仕様に適合したものであるか否かを検証することが重要となる。このため、算術演算を含む回路と設計仕様との等価性検証を行う技術が知られている。
【０００３】
例えば、非特許文献１には、有限桁で閉じた整数演算器の形式検証を、ガロア体ＧＦ（２
ｍ
）上の乗算器検証に適用し、ｍ＝１６３までの検証が可能である技術が開示されている。非特許文献２には、ブール多項式を計算機内で効率よく保持しかつ効率よくその演算を計算するため、ゼロサプレス型二分決定グラフＺＤＤ（Zero-suppressed binary Decision Diagram）を適用し、ガロア体ＧＦ（２
ｍ
）上の乗算器の実装であるｂ－ＳＭＰＯ（Sequential Multiplier with Parallel Output）_Ｉ、ＡＧ－ＳＭＰＯについてはｍ＝４１０まで検証可能である技術が開示されている。非特許文献３には、ＺＤＤを用いた検証アルゴリズムを改良し、検証時間をさらに大幅に短縮する技術が開示されている。
【先行技術文献】
【特許文献】
【０００４】
J. Lv, P. Kalla and F. Enescu, “Efficient Grobner Basis Reductions for Formal Verification of Galois Field Arithmetic Circuits,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol.32, no.9, Sept. 2013.
U. Gupta, P. Kalla and V. Rao, “Boolean Groner Basis Reductions on Finite Field Datapath Circuits Using the Unate Cube Set Algebra,” IEEE Transactions of Computer-Adid Design of Integrated Circuits and Systems, vol. 38, no.3, March 2019.
A. Ito, R. Ueno and N. Homma, “Efficient Formal Verification of Galois-Field Arithmetic Circuits Using ZDD Representation of Boolean Polynomials,” IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, vol 41, no.3, March 2022.
【発明の概要】
【発明が解決しようとする課題】
【０００５】
しかしながら、上記非特許文献１～３のものは、算術演算回路と設計仕様との等価性検証を行う場合に、該算術演算回路を形成する組合せ論理回路のみからなるデータパスについての等価性検証は行っているが、算術演算回路の制御を行うデータパス周辺の順序回路については等価性検証の対象とされていない。その結果、組合せ論理回路及び順序回路を含む算術演算回路と設計仕様の等価性検証を実施することができないという問題があった。
【０００６】
本発明は、上記従来技術による問題点（課題）を解決するためになされたものであって、組合せ論理回路及び順序回路を含む算術演算回路と設計仕様との等価性検証を効率的に行うことができる等価性検証装置、等価性検証方法及び等価性検証プログラムを提供することを目的とする。
【課題を解決するための手段】
【０００７】
上述した課題を解決し、目的を達成するため、本発明は、組合せ論理回路及び順序回路を含む算術演算回路のネットリストと、設計仕様の仕様記述との等価性を計算機代数により検証する等価性検証装置であって、前記ネットリストと前記仕様記述に含まれるタイミングチャートに基づいて第１のブール多項式を生成する第１の生成手段と、前記仕様記述に含まれる論理関数に基づいて第２のブール多項式を生成する第２の生成手段と、前記第１の生成手段により生成された前記第１のブール多項式と、前記第２の生成手段により生成された前記第２のブール多項式の差分を算出する算出手段と、前記算出手段により算出された差分に基づいて、前記ネットリストと前記仕様記述との等価性を判定する判定手段とを備えたことを特徴とする。
【０００８】
また、本発明は、上記発明において、前記第１の生成手段は、前記タイミングチャートに基づいて前記ネットリストが示す前記算術演算回路を動作させた場合に、前記算術演算回路への複数の入力と該算術演算回路内の前記順序回路からの複数の出力とを変数とした第１のブール多項式を生成することを特徴とする。
【０００９】
また、本発明は、上記発明において、前記第１の生成手段は、前記タイミングチャートのクロックの立ち上がりエッジ直前の前記算術演算回路への複数の入力と、前記立ち上がりエッジ直前の該算術演算回路内の前記順序回路からの複数の出力とを変数とした第１のブール多項式を生成することを特徴とする。
【００１０】
また、本発明は、上記発明において、前記判定手段は、前記算出手段により算出された差分が０である場合に、前記ネットリストと前記仕様記述とが等価であると判定することを特徴とする。
（【００１１】以降は省略されています）

関連特許