代数的手法を用いた同期式順序回路の段階的設計法
スポンサーリンク
概要
- 論文の詳細を見る
代数的手法を用いて信頼性の高い同期式順序回路を設計する一つの方法を提案する.提案する手法は,抽象的な要求仕様を記述するレベルから,段階的に設計を行い,レジスタ転送レベルや論理設計レベルの仕様を得るものである.各抽象レベルにおける回路はいわゆる状態図で表すことができ,回路の仕様を代数的言語ASLを用いて形式的かつ厳密に記述する.各段階における設計は,設計者が用いる部品や動作アルゴリズムを自由に決定し,それらを用いて,上位レベルの状態図の各枝が表す抽象的な一動作をより具体的な動作の系列で展開し,下位レベルの状態図を得ることにより行われる.設計の正しさは,展開する動作系列が上位レベルの各一動作を実現しているということであり,この証明を支援系を用いて形式的に行う.また,支援系を用いて,自動合成して得られた下位レベルの状態図を簡約することにより実行効率の良い回路が得られる.論理設計レベルでは,設計者が,用いる部品の機能やバスアーキテクチャなどを決定し,支援系を用いて入力論理およびマイクロプログラムの合成を行う.
- 社団法人電子情報通信学会の論文
- 1994-03-25
著者
-
北道 淳司
大阪大学大学院基礎工学研究科
-
東野 輝夫
大阪大学基礎工学部情報科学科
-
谷口 健一
大阪大学基礎工学部情報科学科
-
東野 輝夫
大阪大学大学院情報科学研究科|独立行政法人科学技術振興機構 Crest
-
北道 淳司
大阪大学基礎工学部情報工学科
-
杉山 裕二
岡山大学工学部通信ネットワーク工学科
-
杉山 裕二
岡山大学工学部
-
谷口 健一
大阪大学基礎工学部情報工学科
関連論文
- 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 におけるレイアウト情報管理用支援ツールの設計
- 整数制約論理のための二分決定グラフの拡張データ構造とそれに対するアルゴリズムの提案
- 遷移の選択が状態訪問回数で決まる有限状態機械対からなる通信系に対する生存性の検証
- 通信プロトコルのLOTOS仕様から並行EFSM群への変換の一手法
- 遷移の選択が状態訪問回数に依存する有限状態機械対からなる通信系に対する生存性検証システム
- 最小p-準クリーク被覆問題に対するハードウェアアルゴリズム(システム設計・開発,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 動的再構成デバイスPCA上での自己複製型アプリケーション設計容易化手法の提案と実装(ハードウェアアルゴリズム, FRGAとその応用及び一般)
- 動的再構成デバイスPCA上での自己複製型アプリケーション設計容易化手法の提案と実装(ハードウェアアルゴリズム, FRGAとその応用及び一般)
- N次元高速アダマール変換アルゴリズムの提案と動的再構成可能デバイスへの実装(FPGAとその応用及び一般)
- N次元高速アダマール変換アルゴリズムの提案と動的再構成可能デバイスへの実装(FPGAとその応用及び一般)
- 複数の制御部を持つ同期式順序回路の一設計検証法
- 複数モジュールにより構成される回路仕様に対する効率的な形式的検証法
- 複数モジュールにより構成される回路仕様に対する効率的な形式的検証法
- ニューロ・GAによるデータ転送路最適化問題解法の提案
- 代数的手法を用いた複数の制御部を持つ同期式順序回路に対する設計および検証支援系の開発
- 代数的手法によるPCIバスコントローラの設計検証
- シストリックアレーによる回路設計の正しさの一証明法
- 代数的手法を用いた同期式順序回路の設計支援機能の統合
- グループワークを考慮した協調計算システムにおける動作プログラム群の生成と分散実行
- 遷移条件が状態訪問回数に依存する有限状態機械の生存性検証
- 共有メモリ型並列計算機上での正則な項書換え系の一実装法
- 拡張有限状態機械とペトリネットを表示編集できるGUIツールの作成と応用例 (第54回全国大会 (平成9年前期 於 : 千葉工大) 大会優秀賞受賞論文 (11件)
- レジスタ付きペトリネットを用いた全体動作仕様から分散動作仕様の自動合成とその応用 (コンカレント・コラボレーション技術論文小特集)
- レジスタ付き時間ペトリネットで記述された分散システムの時間制約付き全体仕様からその時間制約を満たす各ノードの動作記述の自動導出(並列・分散)
- あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法
- 関係データベースを用いた在庫管理プログラムの記述とその詳細化の正しさの証明
- リンクの故障を考慮に入れた分散システムの動作仕様の自動導出
- ペトリネットモデルを用いたソフトウェアプロセスの記述とその分散実行制御
- レジスタを持つ自由選択ネットで記述された分散システムの要求仕様から各ノードの動作仕様の導出
- 協調計算システムの動作仕様群の分散実行系
- ASLプログラム開発システムにおける検証の自動化について
- 拡張有限状態機械で記述された協調計算プログラムとその実行系
- 順序機械型プログラムの階層的設計法と在庫管理プログラムの開発例
- 拡張有限状態機械モデルを用いた分散システムの要求仕様から各ノードの動作仕様の自動導出
- 部分項の評価順が指定できる項書換え系とその性質について(計算機構とアルゴリズム)
- 代数的言語ASLを用いた酒屋在庫管理の要求仕様記述
- あるクラスのOut-of-Order型パイプラインCPUの設計の正しさの十分条件とその形式的検証 (電子システムの設計技術と設計自動化)
- 複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法 (機能論理設計, アーキテクチャ設計支援と一般)
- 無線通信網のリンクスケジューリング問題に対する二段階近似解法の提案
- 安定結婚問題を対象とした離散型ニューラルネットワーク解法の性能評価
- システム設計レベルにおける回路の性質検証のための整数データを処理可能なCTLモデル検査法の提案と実装
- 代数的手法を用いたハードウェアの仕様記述とその詳細化について(計算アルゴリズムと計算量の基礎理論)
- in-order実行パイプラインCPUの正しさの自動証明例
- 静的マルチキャストルーティング問題に対する最適パス選択解法の提案
- FDTって何?(コンピュータと通信)
- すべての変数が存在記号で束縛された冠頭標準形プレスブルガー文の真偽判定の高速化手法
- プレスブルガー文真偽判定手続きを用いた算術演算回路の正しさの証明
- 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設計技術,一般セッション)
- 複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法 (機能論理設計, アーキテクチャ設計支援と一般)