モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法(プロセッサ, DSP, 画像処理技術及び一般)
スポンサーリンク
概要
- 論文の詳細を見る
本論文では, ハードウェアインターフェース仕様全体をより包括的に検証することを目指し, 正規表現ベースの仕様記述言語からモニタ回路を生成する手法を示す.モニタ回路の生成は自動的に行われるため, 複雑な仕様に対するモニタ回路であっても人手で設計する場合に比べ, 誤りの混入を避けることができる.また, モジュール単位の検証の際, 通常では入力制約を付加する必要があるが, 本論文では仕様記述から, 入力制約を自動的に抽出して, モニタ回路に直接反映させる手法について述べる.実験では設計例としてバスプロトコルであるAMBA AHBに従って設計された回路を取り上げ, 実際に仕様を記述してモニタを生成し, 形式検証を行った結果を示す.
- 社団法人電子情報通信学会の論文
- 2005-10-14
著者
-
北嶋 暁
大阪電気通信大学総合情報学部情報工学科
-
浜口 清治
大阪大学大学院情報科学研究科
-
柏原 敏伸
大阪大学大学院情報科学研究科
-
垣内 洋介
大阪大学大学院情報科学研究科
-
垣内 洋介
大阪大学 大学院情報科学研究科
-
柏原 敏伸
大阪大学大学院
-
北嶋 暁
大阪電気通信大学 総合情報学部情報工学科
-
北嶋 暁
大阪電気通信大学総合情報学部メディアコンピュータシステム学科
-
浜口 清治
大阪大学大学院基礎工学研究科
関連論文
- 第一階述語論理のサブクラスに対する近似的モデル検査アルゴリズム (ディペンダブルコンピューティング)
- 第一階述語論理のサブクラスに対する近似的モデル検査アルゴリズム (VLSI設計技術)
- メッセージ・シークエンス・チャートに対するSATソルバーを用いたディスコード計算手法 (ディペンダブルコンピューティング)
- メッセージ・シークエンス・チャートに対するSATソルバーを用いたディスコード計算手法 (コンピュータシステム)
- JPEG2000用ウェーブレット変換器のアーキテクチャ設計とその評価
- stグラフの道独立頂点集合の性質
- データタイプを考慮したASIP消費電力見積り手法の提案
- データタイプを考慮したASIP消費電力見積り手法の提案
- 命令インタリーブ発行機構を有するマルチスレッド向けプロセッサの提案
- 第一階述語論理のサブクラスに対する近似的モデル検査アルゴリズム
- メッセージ・シークエンス・チャートに対するSATソルバーを用いたディスコード計算手法
- メッセージ・シークエンス・チャートに対するSATソルバーを用いたディスコード計算手法
- メッセージ・シークエンス・チャートに対するSATソルバーを用いたディスコード計算手法
- メッセージ・シークエンス・チャートに対するSATソルバーを用いたディスコード計算手法
- CPU設計導入教育への形式的設計検証手法の適用
- メッセージ・シークエンス・チャートに対するSATソルバーを用いたディスコード計算手法
- メッセージ・シークエンス・チャートに対するSATソルバーを用いたディスコード計算手法
- メッセージ・シークエンス・チャートに対するSATソルバーを用いたディスコード計算手法
- マークグラフにおけるトランジションの潜在的同時発火可能性判定アルゴリズム
- 1-有界無競合ペトリネットにおける二つのトランジションの同時発火可能性を判定するYenのアルゴリズムの改良
- マークグラフにおけるトランジションの潜在的同時発火可能性判定アルゴリズム
- ペトリネットの部分クラスにおける同時発火可能性
- しきい値関数を表す共有2分決定グラフの最適な変数順序付けの計算複雑度
- 局所変数を含むアサーションに対するモデルチェッキングのためのチェッカ生成(アサーションベース検証,システム設計及び一般)
- 局所変数を含むアサーションに対するモデルチェッキングのためのチェッカ生成(システム設計及び一般)
- 動的局所変数を含むアサーションに対する限定モデルチェッキング(デザインガアイ2006-VLSI設計の新しい大地を考える研究会)
- 動的局所変数を含むアサーションに対する限定モデルチェッキング(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 動的局所変数を含むアサーションに対する限定モデルチェッキング(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 分割統治法による形式的機能検証のためのインタフェイスプロトコルに対するアサーションの分割(設計・検証, FRGAとその応用及び一般)
- アサーションベース検証の基礎とそのねらい(設計・検証, FRGAとその応用及び一般)
- 分割統治法による形式的機能検証のためのインタフェイスプロトコルに対するアサーションの分割(設計・検証, FRGAとその応用及び一般)
- アサーションベース検証の基礎とそのねらい(設計・検証, FRGAとその応用及び一般)
- 分割統治法による形式的機能検証のためのインタフェイスプロトコルに対するアサーションの分割(設計・検証, FRGAとその応用及び一般)
- アサーションベース検証の基礎とそのねらい(設計・検証, FRGAとその応用及び一般)
- 大規模回路設計に対するフォーマル仕様記述・検証技術の現状と動向
- 第一階述語論理のサブクラスに対する項の高さ縮減を用いた不変条件の近似的検証アルゴリズム(テストと検証,デザインガイア2007-VLSI設計の新しい大地を考える研究会-)
- 第一階述語論理のサブクラスに対する項の高さ縮減を用いた不変条件の近似的検証アルゴリズム(テストと検証,デザインガイア2007-VLSI設計の新しい大地を考える研究会-)
- 第一階述語論理のサブクラスに対する項の高さ縮減を用いた不変条件の近似的検証アルゴリズム(テストと検証,デザインガイア2007-VLSI設計の新しい大地を考える研究会-)
- 同値制約を考慮した第一階述語論理の決定可能なサブクラスによる等価性判定(デザインガアイ2006-VLSI設計の新しい大地を考える研究会)
- 同値制約を考慮した第一階述語論理の決定可能なサブクラスによる等価性判定(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 同値制約を考慮した第一階述語論理の決定可能なサブクラスによる等価性判定(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 定数幅量子ブランチングプログラムの計算能力 (計算理論とアルゴリズムの新展開)
- 1回読み定数幅制約下での量子ブランチングプログラムと確率ブランチングプログラムの計算能力の比較
- クロネッカー式関数決定グラフの最適展開規則選択問題の計算複雑度(情報基礎理論ワークショップ(LAシンポジウム)論文小特集)
- 二分モーメントグラフによる除算表現の大きさの指数下界 (アルゴリズムと計算の理論)
- 二分モーメントグラフによる除算表現の大きさの指数下界
- 妨害者のいる場合の最短経路問題
- 妨害の下での最短経路問題の複雑さ : 通過後の妨害を許さない場合
- 円筒上長方形交グラフの最大クリークを求めるアルゴリズム
- 妨害の下での最短経路問題
- パスグラフから区間グラフへの最小辺付加による変換の NP 完全性
- 交互シャフルについて
- 木上二重コンベックスグラフと二部サークルグラフの等価性
- 端子間に配線を通過させない順列配線のビア数最小化アルゴリズム
- 円筒上長方形交グラフの最大クリークを求めるアルゴリズム
- パスグラフから区間グラフへの最小辺付加による変換のNP完全性
- ある種のグラフにおける最大クリーク重みの折点数について
- モニタベース手法を用いたオン・チップ・バスプロトコルの機能検証に関する研究(研究会推薦博士論文速報)
- モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法(ハードウェア,フォーマルアプローチ論文)
- モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法(プロセッサ, DSP, 画像処理技術及び一般)
- モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法(プロセッサ, DSP, 画像処理技術及び一般)
- モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法(プロセッサ, DSP, 画像処理技術及び一般)
- モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法(プロセッサ, DSP, 画像処理技術及び一般)
- 平面グラフの最大重み窓問題
- 外窓上の頂点および辺の重みの和を最大にするような,2連結平面グラフの描写アルゴリズム
- 第一階述語論理のサブクラスを利用したブール関数レベルの等価性判定手法(FPGAとその応用及び一般)
- 第一階述語論理のサブクラスを利用したブール関数レベルの等価性判定手法(FPGAとその応用及び一般)
- 第一階述語論理のサブクラスを利用したブール関数レベルの等価性判定手法(FPGAとその応用及び一般)
- 第一階述語論理のサブクラスを利用したブール関数レベルの等価性判定手法(FPGAとその応用及び一般)
- コンパラビリティグラフから得られるst有向グラフのセパレータ
- An Algorithm for Generating Maximum Weight Independent Sets in a Circle Graph
- パラメトリックグラフにおける最大クリ-ク重みの折れ点数
- 2層配線における3端子ネットの分割
- 部品の端子間に配線を通過させない一層配線問題について
- 部品の反転を許さない一層平面配線問題について
- トランザクション識別子を伴うバスプロトコル間の変換器自動生成手法 (ディペンダブルコンピューティング)
- トランザクション識別子を伴うバスプロトコル間の変換器自動生成手法 (コンピュータシステム)
- 特定用途向きプロセッサ開発システムASIP Meister
- 特定用途向きプロセッサ開発システム ASIP Meister
- 特定用途向きプロセッサ開発システムASIP Meister
- JPEG2000用ウェーブレット変換器のアーキテクチャ設計とその評価
- digitシリアル演算を用いたDSPシステム設計最適化の一手法
- digitシリアル演算を用いたDSPシステム設計最適化の一手法
- digitシリアル演算を用いたDSPシステム設計最適化の一手法
- ASIP開発システムPEAS-IIIのための命令セットレベルシミュレータの自動生成
- ASIP開発システムPEAS-IIIのための命令セットレベルシミュレータの自動生成
- パイプライン段数を考慮したASIP設計最適化の検討
- VHDLで記述されたシステム仕様のプロセスレベルでのHW/SW分割の一手法
- VHDLで記述されたシステム仕様のプロセスレベルでのHW/SW分割の一手法
- VHDLで記述されたシステム仕様のプロセスレベルでのHW/SW分割の一手法
- トランザクション識別子を伴うバスプロトコル間の変換器自動生成手法
- トランザクション識別子を伴うバスプロトコル間の変換器自動生成手法
- 第一階述語論理の決定可能なサブクラスに対する同値制約を考慮した充足可能性判定(検証・理論, 組込技術とネットワークに関するワークショップ)
- 第一階述語論理の決定可能なサブクラスに対する同値制約を考慮した充足可能性判定
- 第一階述語論理の決定可能なサブクラスに対する同値制約を考慮した充足可能性判定(検証・理論, 組込技術とネットワークに関するワークショップ)
- VLIWプロセッサにおける演算命令発行スロット数の最適化
- VLIWプロセッサにおける演算命令発行スロット数の最適化
- VLIWプロセッサ自動生成における演算器構成最適化の一手法
- VLIWプロセッサ自動生成における演算器構成最適化の一手法
- A-3-8 メモリを用いた算術演算回路のFPGA実現とその電力評価(A-3.VLSI設計技術,一般セッション)