複数の制御部を持つ同期式順序回路の一設計検証法
スポンサーリンク
概要
- 論文の詳細を見る
複数の制御部を持つ同期式順序回路の設計の正しさを保証するための形式的手法を用いた一設計検証法を提案する.本手法は, 抽象度が高く1つの制御部で実現されている回路(以下, 上位レベルの回路)が与えられ, より抽象度が低く複数の制御部で実現されている回路(以下, 下位レベルの回路)を設計し, 上位レベルの回路と下位レベルの回路との間の対応を与えたときに, 下位レベルの回路が対応のもとで上位レベルの回路を正しく実現していることを証明する方法である.複数の制御部を持つ回路を検証する場合, 各制御部の直積機械を生成するという手法が一般的であるが, この手法では計算時間および計算空間が増大し, 大規模な回路の場合は検証が不可能である.本手法では、上位レベルの回路の各状態遷移に対して, 状態を持つ部品ごとに下位レベルの回路の状態遷移系列を設計者が対応づけ, 上位レベルの回路の状態遷移ごとにレジスタ転送や制御構造などが正しく実現されていることを局所的に証明することにより, 各制御部の直積機械を生成することなく検証を行う.本手法をPCIバスを介してCPUモジュールとメモリモジュールを接続する回路に適用した.この例の回路規模は制御部数9, 遷移数96であった.証明が成功したときのCPU時間は約20分であった.
- 一般社団法人情報処理学会の論文
- 1998-07-15
著者
-
北道 淳司
大阪大学大学院基礎工学研究科
-
西川 清史
大阪大学大学院基礎工学研究科情報数理系専攻
-
竹中 崇
大阪大学大学院基礎工学研究科情報数理系専攻
-
竹中 崇
大阪大学大学院情報科学研究科:(現)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 におけるレイアウト情報管理用支援ツールの設計
- 整数制約論理のための二分決定グラフの拡張データ構造とそれに対するアルゴリズムの提案
- 最小極大マッチング問題のニューラルネットワーク並列解法の提案
- 組合せ最適化問題に対する離散値ニューラルネットワーク解法の安定性の一考察
- Minimum Maximal Matching問題のニューラルネットワーク解法の提案
- 最小p-準クリーク被覆問題に対するハードウェアアルゴリズム(システム設計・開発,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 動的再構成デバイスPCA上での自己複製型アプリケーション設計容易化手法の提案と実装(ハードウェアアルゴリズム, FRGAとその応用及び一般)
- 動的再構成デバイスPCA上での自己複製型アプリケーション設計容易化手法の提案と実装(ハードウェアアルゴリズム, FRGAとその応用及び一般)
- N次元高速アダマール変換アルゴリズムの提案と動的再構成可能デバイスへの実装(FPGAとその応用及び一般)
- N次元高速アダマール変換アルゴリズムの提案と動的再構成可能デバイスへの実装(FPGAとその応用及び一般)
- 複数の制御部を持つ同期式順序回路の一設計検証法
- 複数モジュールにより構成される回路仕様に対する効率的な形式的検証法
- 複数モジュールにより構成される回路仕様に対する効率的な形式的検証法
- ニューロ・GAによるデータ転送路最適化問題解法の提案
- 代数的手法を用いた複数の制御部を持つ同期式順序回路に対する設計および検証支援系の開発
- 代数的手法によるPCIバスコントローラの設計検証
- シストリックアレーによる回路設計の正しさの一証明法
- 代数的手法を用いた同期式順序回路の設計支援機能の統合
- 無線通信網の通信経路割当て問題を対象としたグリーディニューラルネットワーク解法の提案
- マルチキャストパケット交換方式におけるワンショットスケジューリング問題のニューラルネットワーク解法
- N-Queen問題を対象としたマキシマムニューロンモデルの競合解消方式の提案
- グラフ分割問題に対するバイナリーニューロンを用いたニューラルネットワーク解法
- 無線通信網の通信経路割当問題に対するグリーディ・ニューラルネットワーク解法の提案
- マキシマム・ニューラルネットワークによる無線通信網の通信経路選択法の提案
- マキシマムニューロンを用いた安定結婚問題のニューラルネットワーク解法
- 巡回セールスマン問題を対象としたニューロンフィルタの提案
- N-Queen問題を対象としたニューラルネットワークの半同期式更新方式の提案
- ニューラルネットワークによるセルラー通信網のチャンネル割当問題の一解法の研究
- バイナリニューロンを用いたグラフ分割解法の研究
- 巡回セールスマン問題の従来アルゴリズムの評価と新しいニューラルネットワークアルゴリズムの提案
- N-Queen問題を対象としたマキシマムニューロンモデルの"Winner-take-all"方式に関する研究
- 無線通信網における通信経路選択問題のマキシマム・ニューロンを用いたニューラルネットワーク解法の提案
- マキシマムニューロンを用いたN-Queen問題のニューラルネット解法の提案
- グラフ分割問題に対するニューラルネットワーク解法の提案
- ウインドウ付きマルチキャスト・パケット交換方式におけるワンショット・スケジューリング問題のニューラルネット解法
- ASLプログラム開発システムにおける検証の自動化について
- 順序機械型プログラムの階層的設計法と在庫管理プログラムの開発例
- あるクラスのOut-of-Order型パイプラインCPUの設計の正しさの十分条件とその形式的検証 (電子システムの設計技術と設計自動化)
- 複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法 (機能論理設計, アーキテクチャ設計支援と一般)
- 安定結婚問題を対象とした離散型ニューラルネットワーク解法の性能評価
- 安定結婚問題のニューラルネットワーク解法の提案
- システム設計レベルにおける回路の性質検証のための整数データを処理可能なCTLモデル検査法の提案と実装
- 代数的手法を用いたハードウェアの仕様記述とその詳細化について(計算アルゴリズムと計算量の基礎理論)
- 静的マルチキャストルーティング問題に対する最適パス選択解法の提案
- FPGA配線問題に対する貪欲法とニューラルネットワークを併用した3段階アルゴリズムの提案
- マルチキャスト・パケット交換方式におけるユニキャストおよびマルチキャスト問題のニューラルネットワーク解法
- ニューラルネットワークによるマルチキャスト・パケット・スイッチ制御アルゴリズムの研究
- 観測不可能な非決定動作を含む並行DFSM群としてモデル化される通信プロトコルの適合性試験法(マルチメディアコミュニケーションシステム)
- 代数的言語ASLによる回路設計支援システムにおけるSFL記述への詳細化とその変更及びそれらの正しさの検証
- 貪欲法とGAを併用したデータ転送路資源最適化問題解法の提案
- DS-1-2 チャネル割当て問題に対するニューラルネットワークアルゴリズムの改良手法(DS-1.計算理論における学生の研究パワー:COMP学生シンポジウム,シンポジウムセッション)
- プログラムの処理速度調整に基づいたデータセンタ向け省電力タスクスケジューリング法
- 高位設計における形式的検証のための整数上の制約論理式の真偽判定プログラムに対する改良手法
- 高位設計における形式的検証のための整数上の制約論理式の真偽判定プログラムに対する改良手法
- 高位設計における形式的検証のための整数上の制約論理式の真偽判定プログラムに対する改良手法
- プレスブルカー文真偽判定アルゴリズムのためのBDDの応用とそれを用いた回路検証 (電子システムの設計技術と設計自動化)
- 大型計算機センタの役割
- マルチコンテキストFPGAのためのコンテキスト分割アルゴリズムの実例による評価
- マルチコンテキストFPGAのためのコンテキスト分割アルゴリズムの実例による評価
- マルチコンテキストFPGAのためのコンテキスト分割アルゴリズムの実例による評価
- SMIL風シナリオ群からのQoSを考慮したプロトコル合成
- SMIL風シナリオ群からのQoSを考慮したプロトコル合成
- 代数的言語で記述した抽象的順序機械型プログラムの設計検証の自動化
- 整数上の論理式の恒真性判定アルゴリズムを用いた組合せ論理回路の実現の正しさの証明
- LOTOS風言語で書かれた同期式順序回路の要求仕様記述と回路自動合成
- 代数的手法を用いた同期式順序回路の段階的設計法
- 並列実行される動作におけるデータ代入の衝突の判定
- 整数上の線形制約の処理と応用 (制約論理プログラミング)
- 代数的手法を用いた順序回路設計支援システムにおける検証支援機能と検証手順
- 代数的手法を用いた回路設計支援システムにおける状態図簡約機能とその評価
- マルチアクセラレータ型動的再構成プロセッサの実装(FPGAアクセラレーター,FPGA応用及び一般)
- マルチアクセラレータ型動的再構成プロセッサの実装(FPGAアクセラレーター,FPGA応用及び一般)
- マルチアクセラレータ型動的再構成プロセッサの実装(FPGAアクセラレーター,FPGA応用及び一般)
- FPGA配線問題に対する貪欲法とニューラルネットワークを併用した3段階アルゴリズムの提案
- セルラー通信網のあるチャンネル割当問題に対するマキシマムニューラルネットワーク解法の提案
- 移植が容易なPCI Expressインターフェイスフレームワークの設計と実装(FPGA応用)
- 動的再構成可能FPGAの設計とそれへの並列アルゴリズムの実装
- FPGA上で動作可能なマルチプロセッサRTOSの提案
- FPGA上で動作可能なマルチプロセッサRTOSの提案
- 5. 代数的手法による仕様記述と設計および検証 ( 論理設計の形式的検証)
- 代数的手法を用いたマイクロプログラム制御方式順序回路の階層的設計
- ターボブースト・ハイパースレッディングを考慮したマルチコアプロセッサ向けタスクスケジューリング
- A-3-13 電力消費の評価のためのARMプロセッサの実装(A-3.VLSI設計技術,一般セッション)
- 複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法 (機能論理設計, アーキテクチャ設計支援と一般)