複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法 (<特集>機能論理設計, アーキテクチャ設計支援と一般)
スポンサーリンク
概要
- 論文の詳細を見る
高位設計における複数の制御部を持つ同期式順序回路を対象とする, 不変式の証明を用いた一形式的検証法を提案する. 不変式とは設計者あるいは検証者が回路の動作中にレジスタや制御信号などの間に成り立つと考える関係である. 回路記述は, 複数の有限状態部 (制御部) とそれらが制御するデータパスからなる. 不変式は各制御部の任意の有限状態に設定することができる. 制御部における実行条件, データパスにおける演算および不変式は, 論理型, 整数型, ユーザが定義したデータタイプの変数および関数などを用いて記述することができる. 検証は, いくつかの不変式, データパス, 実行条件, ユーザ定義関数に関する補題を前提として, 証明すべき不変式を証明するという, 有限状態に関する構造的帰納法を用いて行う. この証明作業は, 各制御部と等価な直積制御部を生成しその上で行う. 直積制御部の生成時に到達不能な状態の削減をはかる. プレスブルガー文真偽判定ルーチンを利用して, 証明すべき式の十分粂件を判定する. 本手法の有用性をPCIバスインターフェース回路を用いて評価する.
- 一般社団法人情報処理学会の論文
- 1997-12-11
著者
-
北道 淳司
大阪大学大学院基礎工学研究科
-
船曵 信生
大阪大学大学院基礎工学研究科情報数理系専攻
-
竹中 崇
大阪大学大学院基礎工学研究科情報数理系専攻
-
竹中 崇
大阪大学大学院情報科学研究科:(現)necマルチメデイア研究所
-
齊藤 義勝
大阪大学大学院基礎工学研究科情報数理系専攻
-
竹中 崇
日本電気株式会社システムIPコア研究所
-
竹中 崇
日本電気株式会社
関連論文
- D-3-4 UMLを用いた組込みOS:TOPPERS/JSPのモデリング(D-3. ソフトウェアサイエンス,一般セッション)
- 災害医療支援ネットワークのための軽傷者用負傷者端末(システム設計,物理設計及び一般)
- FPGAを用いた2次元液体運動シミュレーションの高速化(リコンフィギャラブル応用)
- SystemCを用いた動的再構成可能プロセッサのモデル開発(システム設計及び一般)
- SystemCを用いた動的再構成可能プロセッサのモデル開発(Cベース設計事例,システム設計及び一般)
- D-18-4 バタフライネットワークの部分再構成デバイスへの実装(D-18.リコンフィギャラブルシステム,一般講演)
- 最小p-準クリーク被覆問題に対するハードウェアアルゴリズム(デザインガアイ2006-VLSI設計の新しい大地を考える研究会)
- 最小p-準クリーク被覆問題に対するハードウェアアルゴリズム(システム設計・開発,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- A-1-24 PCA上の領域の有効利用を目的とした処理ユニットの設計と実装(A-1.回路とシステム,基礎・境界)
- 動的再構成可能デバイスPCA-2への逆誤差伝搬法の実装(リコンフィギャラブル応用II, リコンフィギャラブルシステム, 一般)
- 動的再構成デバイスPCA上での自己複製型アプリケーション設計容易化手法の提案と実装(ハードウェアアルゴリズム, FRGAとその応用及び一般)
- PCAにおける部分再構成機能を利用したウェーブレット変換回路の設計(アプリケーションI)(リコンフィギャラブルシステムにおける設計技術及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- SystemCを用いた動的再構成可能アーキテクチャPCAのためのシミュレーション法の提案(システム設計及び一般)
- SystemCを用いた動的再構成可能アーキテクチャPCAのためのシミュレーション法の提案(システム設計および一般)
- N次元高速アダマール変換アルゴリズムの提案と動的再構成可能デバイスへの実装(FPGAとその応用及び一般)
- A-3-20 Plastic Cell Architecture におけるレイアウト情報管理用支援ツールの設計
- 整数制約論理のための二分決定グラフの拡張データ構造とそれに対するアルゴリズムの提案
- 外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
- Minimum Maximal Matching問題のニューラルネットワーク解法の提案
- 最小p-準クリーク被覆問題に対するハードウェアアルゴリズム(システム設計・開発,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 動的再構成デバイスPCA上での自己複製型アプリケーション設計容易化手法の提案と実装(ハードウェアアルゴリズム, FRGAとその応用及び一般)
- 動的再構成デバイスPCA上での自己複製型アプリケーション設計容易化手法の提案と実装(ハードウェアアルゴリズム, FRGAとその応用及び一般)
- N次元高速アダマール変換アルゴリズムの提案と動的再構成可能デバイスへの実装(FPGAとその応用及び一般)
- N次元高速アダマール変換アルゴリズムの提案と動的再構成可能デバイスへの実装(FPGAとその応用及び一般)
- 複数の制御部を持つ同期式順序回路の一設計検証法
- 複数モジュールにより構成される回路仕様に対する効率的な形式的検証法
- 複数モジュールにより構成される回路仕様に対する効率的な形式的検証法
- ニューロ・GAによるデータ転送路最適化問題解法の提案
- 代数的手法を用いた複数の制御部を持つ同期式順序回路に対する設計および検証支援系の開発
- 代数的手法によるPCIバスコントローラの設計検証
- シストリックアレーによる回路設計の正しさの一証明法
- 代数的手法を用いた同期式順序回路の設計支援機能の統合
- グラフ分割問題に対するバイナリーニューロンを用いたニューラルネットワーク解法
- マキシマム・ニューラルネットワークによる無線通信網の通信経路選択法の提案
- 巡回セールスマン問題を対象としたニューロンフィルタの提案
- ASLプログラム開発システムにおける検証の自動化について
- 順序機械型プログラムの階層的設計法と在庫管理プログラムの開発例
- あるクラスのOut-of-Order型パイプラインCPUの設計の正しさの十分条件とその形式的検証 (電子システムの設計技術と設計自動化)
- 複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法 (機能論理設計, アーキテクチャ設計支援と一般)
- 安定結婚問題を対象とした離散型ニューラルネットワーク解法の性能評価
- システム設計レベルにおける回路の性質検証のための整数データを処理可能なCTLモデル検査法の提案と実装
- 代数的手法を用いたハードウェアの仕様記述とその詳細化について(計算アルゴリズムと計算量の基礎理論)
- 静的マルチキャストルーティング問題に対する最適パス選択解法の提案
- FPGA配線問題に対する貪欲法とニューラルネットワークを併用した3段階アルゴリズムの提案
- 観測不可能な非決定動作を含む並行DFSM群としてモデル化される通信プロトコルの適合性試験法(マルチメディアコミュニケーションシステム)
- 代数的言語ASLによる回路設計支援システムにおけるSFL記述への詳細化とその変更及びそれらの正しさの検証
- 貪欲法とGAを併用したデータ転送路資源最適化問題解法の提案
- DS-1-2 チャネル割当て問題に対するニューラルネットワークアルゴリズムの改良手法(DS-1.計算理論における学生の研究パワー:COMP学生シンポジウム,シンポジウムセッション)
- プログラムの処理速度調整に基づいたデータセンタ向け省電力タスクスケジューリング法
- 高位設計における形式的検証のための整数上の制約論理式の真偽判定プログラムに対する改良手法
- 高位設計における形式的検証のための整数上の制約論理式の真偽判定プログラムに対する改良手法
- 高位設計における形式的検証のための整数上の制約論理式の真偽判定プログラムに対する改良手法
- プレスブルカー文真偽判定アルゴリズムのためのBDDの応用とそれを用いた回路検証 (電子システムの設計技術と設計自動化)
- マルチコンテキストFPGAのためのコンテキスト分割アルゴリズムの実例による評価
- マルチコンテキストFPGAのためのコンテキスト分割アルゴリズムの実例による評価
- マルチコンテキストFPGAのためのコンテキスト分割アルゴリズムの実例による評価
- FPGAの論理ブロックの端子割当問題の定式化と2段階離散最適化法の提案
- SMIL風シナリオ群からのQoSを考慮したプロトコル合成
- SMIL風シナリオ群からのQoSを考慮したプロトコル合成
- 代数的言語で記述した抽象的順序機械型プログラムの設計検証の自動化
- 整数上の論理式の恒真性判定アルゴリズムを用いた組合せ論理回路の実現の正しさの証明
- LOTOS風言語で書かれた同期式順序回路の要求仕様記述と回路自動合成
- 代数的手法を用いた同期式順序回路の段階的設計法
- 並列実行される動作におけるデータ代入の衝突の判定
- 整数上の線形制約の処理と応用 (制約論理プログラミング)
- 代数的手法を用いた順序回路設計支援システムにおける検証支援機能と検証手順
- 代数的手法を用いた回路設計支援システムにおける状態図簡約機能とその評価
- マルチアクセラレータ型動的再構成プロセッサの実装(FPGAアクセラレーター,FPGA応用及び一般)
- リニアサーチを併用した決定木によるフロー検索ハードウェアエンジン(アプリケーション(1))
- マルチアクセラレータ型動的再構成プロセッサの実装(FPGAアクセラレーター,FPGA応用及び一般)
- マルチアクセラレータ型動的再構成プロセッサの実装(FPGAアクセラレーター,FPGA応用及び一般)
- FPGA配線問題に対する貪欲法とニューラルネットワークを併用した3段階アルゴリズムの提案
- チャネル割当問題を対象とした拡張マキシマムニューラルネットワーク解法の提案
- セルラー通信網のあるチャンネル割当問題に対するマキシマムニューラルネットワーク解法の提案
- 移植が容易なPCI Expressインターフェイスフレームワークの設計と実装(FPGA応用)
- 遺伝的プログラミングを用いた関数合成アルゴリズムの一改良法の提案
- 動的再構成可能FPGAの設計とそれへの並列アルゴリズムの実装
- FPGA上で動作可能なマルチプロセッサRTOSの提案
- FPGA上で動作可能なマルチプロセッサRTOSの提案
- 5. 代数的手法による仕様記述と設計および検証 ( 論理設計の形式的検証)
- C言語設計によるハードウェア複合イベント処理
- C言語設計によるハードウェア複合イベント処理
- 代数的手法を用いたマイクロプログラム制御方式順序回路の階層的設計
- ターボブースト・ハイパースレッディングを考慮したマルチコアプロセッサ向けタスクスケジューリング
- C-12-11 ウェーブレット縮退の多段化によるデノイズ画像処理とそのLSIアーキテクチャ : Part II(C-12.集積回路,一般セッション)
- C-12-10 ウェーブレット縮退の多段化によるデノイズ画像処理とそのLSIアーキテクチャ : Part I(C-12.集積回路,一般セッション)
- A-3-13 電力消費の評価のためのARMプロセッサの実装(A-3.VLSI設計技術,一般セッション)
- 不完全ネストループに対するループパイプライン(暗号と高位設計,システムオンシリコンを支える設計技術)
- 複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法 (機能論理設計, アーキテクチャ設計支援と一般)
- 不完全ネストループに対するループパイプライン
- 二重キャッシングによるMemcached高速化の提案(FPGA応用,FPGA応用及び一般)
- 二重キャッシングによるMemcached高速化の提案(FPGA応用,FPGA応用及び一般)
- 二重キャッシングによるMemcached高速化の提案(FPGA応用,FPGA応用及び一般)