形式的手法を用いたプロセッサ設計不具合の自動診断と修正
スポンサーリンク
概要
- 論文の詳細を見る
本稿ではプロセッサ設計不具合を自動的に診断して修正する手法を提案する.手法は,ある命令セットをもつプロセッサに関して,逐次的に命令を実行して正常動作するモデルと,スーパースカラ・アウトオーブオーダ実行などの高性能化を実現する機構を含むが正常動作しないモデルが与えられた際に,後者のモデルの不具合を診断・修正する.本手法は,従来 RTL 設計やゲートレベルのネットリストのデバッグに用いられてきた,設計に対してマルチプレクサを挿入してその入力信号値を設計が正しく動作するように決定する手法に基づくものとなっている.決定された信号値は不具合を設計する修正の候補を表現し,各修正候補は候補を用いた修正を経た正常動作しないモデルが正常動作するモデルと等価な動作をすることが形式的に検証されると最終的な解として出力される.提案手法を,スーパースカラ・アウトオブオーダ実行や,タイミングエラー回復機構を備えた複雑なプロセッサを例題として評価を行った.評価のためプロセッサに挿入したバグは提案手法により診断・修正可能であることが確認された.
- 2012-12-06
著者
-
藤田 昌宏
東京大学大規模集積システム設計教育研究センター:科学技術振興機構戦略的創造研究推進事業crest
-
谷田 英生
東京大学大学院工学系研究科電気系工学専攻
-
藤田 昌宏
埼玉大学大学院理工学研究科
-
藤田 昌宏
東京大学大規模集積システム設計教育研究センター
-
藤田 昌宏
国立札幌病院
-
藤田 昌宏
東京大学、大規模集積システム設計教育研究センター
関連論文
- 162.前立腺移行上皮癌の一例(前立腺 : 示説, 第28回日本臨床細胞学会秋期大会学術集会)
- I-2-2. リンパ節転移を認めた食道 m 癌の3例(第47回食道疾患研究会)
- 粘膜筋板由来の胃平滑筋肉腫の1例
- 動的パッチ読み出し機構を備えた製造後機能修正可能アクセラレータ (画像工学)
- 動的パッチ読み出し機構を備えた製造後機能修正可能アクセラレータ (集積回路)
- 動的パッチ読み出し機構を備えた製造後機能修正可能アクセラレータ (信号処理)
- 5.手術症例よりみた末梢肺腺癌(2cm以下)の画像診断の特徴と外科治療 : 第24回日本肺癌学会北海道支部会
- 5. 多発胃平滑筋芽細胞腫の 1 例(第 57 回日本小児外科学会北海道地方会)
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバック,組込技術とネットワークに関するワークショップETNET2009)
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバッグ,組込技術とネットワークに関するワークショップETNET2009)
- I-B-10. 巨大な食道ポリープ(fibrovascular polyp, 以下FVP)の1切除例(I. 見て良かった稀な食道疾患)
- 専用プロセッサ用命令セットの自動生成手法の提案と実装
- ハードウェアデバッグ支援のためのエラー入出力トレースの上位レベル設計における再現手法(高位レベルテスト・検証,VLSI設計とテスト及び一般)
- 準形式的モデル検査のハードウェア実装による高速化の検討(モデル・回路,組込技術とネットワークに関するワークショップETNET2008)
- 製造後デバッグのための入出力シーケンススライシング手法(設計/テスト/検証)
- 充足可能性判定に基づくシステムレベルデバッグ支援手法におけるバグモデルの導入による効率化
- 上位設計記述の解析を利用した製造後機能テストの効率化
- 動的パッチ読み出し機構を備えた製造後機能修正可能アクセラレータ
- 依存グラフを用いた局所的な記号シミュレーションによるC言語記述に対する等価性検証手法の提案(システムLSI設計及び一般)
- 依存グラフを用いた局所的な記号シミュレーションによるC言語記述に対する等価性検証手法の提案(システムLSI設計及び一般)
- C言語でのハードウェア記述に対する効率的な等価性検証手法の提案(システム設計及び一般)
- ループ融合を利用した複数のforループからのパイプラインハードウェア合成
- ループ融合を利用した複数の for ループからのパイプラインハードウェア合成
- 1M-5 ワードレベル論理式の充足可能性判定問題を利用したシステムレベル設計デバッグ支援手法(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 専用プロセッサ用命令セットの自動生成手法の提案と実装
- 潜在的多様性を考慮したプログラマブルハードウェアの高位合成手法(プログラマブルデバイスと設計技術,システムオンシリコンを支える設計技術)
- 高性能SoCプロトタイプのFPGA実装方式の検討 (ディペンダブルコンピューティング)
- 高性能SoCプロトタイプのFPGA実装方式の検討 (VLSI設計技術)
- 設計固有セルライブラリの自動生成手法(論理設計,デザインガイア2009-VLSI設計の新しい大地)
- Increasing yield using partially-programmable circuits (VLSI設計技術)
- 設計固有セルライブラリの自動生成手法(論理設計,デザインガイア2009-VLSI設計の新しい大地-)
- Increasing yield using partially-programmable circuits (ディペンダブルコンピューティング)
- チップ内プログラマブル配線向け形式的検証手法(暗号処理回路,システムオンシリコンを支える設計技術)
- リンク長及びレイテンシ制約下でのネットワークオンチップのトポロジ自動生成(ネットワークオンチップ,システムオンシリコンを支える設計技術)
- 内部等価点の推定によるルールベース高位検証の高精度化(高位検証,デザインガイア2008-VLSI設計の新しい大地)
- メモリアクセスおよびリソース共有を行うカスタム命令自動生成手法(FPGA・低消費電力設計・システムレベル合成,システム設計及び一般)
- メモリアクセスおよびリソース共有を行うカスタム命令自動生成手法(FPGA・低消費電力設計・システムレベル合成,システム設計及び一般)
- 充足可能性判定を利用した最適コード生成手法
- 有限状態機械(FSM)とシンボリック状態探索を利用したコード生成手法(システムLSIの設計技術と設計自動化)
- 分割二分決定グラフによる有限状態機械の到達可能性解析の PC クラスタを用いた並列実装手法の提案(設計技術と設計自動化)(情報システム論文)
- 分割二分決定グラフによる有限状態機械の到達可能性解析のPCクラスタを用いた並列実装手法の提案
- 仮想マルチプロセッサモデルに基づく高速SoCプロトタイピング手法(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 仮想マルチプロセッサモデルに基づく高速SoCプロトタイピング手法(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 高性能SoCプロトタイプのFPGA実装方式の検討(論理設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 高性能SoCプロトタイプのFPGA実装方式の検討(論理設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 上位設計記述の解析を利用した製造後機能テストの効率化 (ディペンダブルコンピューティング)
- 上位設計記述の解析を利用した製造後機能テストの効率化 (VLSI設計技術)
- システムレベル設計における並列動作の同期に関するデバッグ支援手法(デバック,組込技術とネットワークに関するワークショップETNET2009)
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバック,組込技術とネットワークに関するワークショップETNET2009)
- システムレベル設計における並列動作の同期に関するデバッグ支援手法(デバック,組込技術とネットワークに関するワークショップETNET2009)
- システムレベル設計における並列動作の同期に関するデバッグ支援手法(デバッグ,組込技術とネットワークに関するワークショップETNET2009)
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバッグ,組込技術とネットワークに関するワークショップETNET2009)
- システムレベル設計における並列動作の同期に関するデバッグ支援手法(デバッグ,組込技術とネットワークに関するワークショップETNET2009)
- 順序回路の上位設計記述における等価性指定の自動化手法(高位検証,FPGA応用及び一般)
- SIDO モデルを用いたブラインド等化に関する一検討(ネットワークプロセッサ, 通信のための信号処理, 符号理論, 一般)
- SIDO モデルを用いたブラインド等化に関する一検討(ネットワークプロセッサ, 通信のための信号処理, 符号理論, 一般)
- SIDOモデルを用いたブラインド等化に関する一検討(ネットワークプロセッサ, 通信のための信号処理, 符号理論, 一般)
- SIDOモデルを用いたブラインド等化に関する一検討
- SIDOモデルを用いたブラインド等化に関する一検討
- SIDOモデルを用いたブラインド等化に関する一検討
- 1M-6 動作合成された束データ方式による非同期式回路とその動作仕様に対する等価性検証手法(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 2分決定グラフを用いた推移的閉包計算アルゴリズムと形式的検証への応用
- Boolean Relationからの多段論理回路の合成
- 大規模回路の多段論理簡単化について
- 発見的手法に基づくスケーラブルなインクリメンタル高位合成(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 発見的手法に基づくスケーラブルなインクリメンタル高位合成(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 2P-1 動的ウェブアプリケーションの操作に対する画面間遷移の網羅的検証(ソフトウェアの検査・検証,学生セッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- インクリメンタル高位合成に向けた設計記述間差分の計算手法 (ディペンダブルコンピューティング)
- インクリメンタル高位合成に向けた設計記述間差分の計算手法 (コンピュータシステム)
- システムレベル設計における同期検証フレームワークの提案
- システムレベル設計における同期検証フレームワークの提案
- データ符号化によるVLSIにおける低消費電力・高信頼データ伝送手法の検討
- データ符号化によるVLSIにおける低消費電力・高信頼データ伝送手法の検討(低消費)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会)
- 準形式的モデル検査のハードウェア実装による高速化の検討(モデル・回路,組込技術とネットワークに関するワークショップETNET2008)
- 準形式的モデル検査のハードウェア実装による高速化の検討(モデル・回路,組込技術とネットワークに関するワークショップETNET2008)
- インクリメンタル高位合成に向けた設計記述間差分の計算手法
- インクリメンタル高位合成に向けた設計記述間差分の計算手法
- 準形式的モデル検査のハードウェア実装による高速化の検討(モデル・回路,組込技術とネットワークに関するワークショップETNET2008)
- 内部等価点の推定によるルールベース高位検証の高精度化(高位検証,デザインガイア2008-VLSI設計の新しい大地)
- 内部等価点の推定によるルールベース高位検証の高精度化(高位検証,デザインガイア2008-VLSI設計の新しい大地-)
- FPGAを用いたSmith-Waterman Algorithmの高速化(科学技術計算)
- 高位合成ツールを利用したハードウェアアルゴリズムの最適化(最適化技術,システム設計及び一般)
- 反例と設計分割に基づく高位設計に対する効率的な設計修正支援手法(検証技術,システム設計及び一般)
- 形式的検証を用いたプロセッサエラー回復機構の耐性評価手法の検討(検証技術,システム設計及び一般)
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討
- 潜在的な依存関係を利用した高位設計デバッグ支援手法 (VLSI設計技術)
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討 (ディペンダブルコンピューティング・組込み技術とネットワークに関するワークショップETNET2012)
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討 (コンピュータシステム・組込み技術とネットワークに関するワークショップETNET2012)
- 動作レベル・レジスタ転送レベル混在設計記述向け高位合成手法 (VLSI設計技術)
- ゲート回路シミュレーションにおけるGPGPUを利用したアサーション自動抽出
- 形式的手法を用いたプロセッサ設計不具合の自動診断と修正
- 形式的手法を用いたプロセッサ設計不具合の自動診断と修正
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討(設計技術,組込み技術とネットワークに関するワークショップETNET2012)
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討(設計技術,組込み技術とネットワークに関するワークショップETNET2012)
- 動作レベル・レジスタ転送レベル混在設計記述向け高位合成手法(動作レベル設計と配線手法,システムオンシリコンを支える設計技術)
- 潜在的な依存関係を利用した高位設計デバッグ支援手法(システム設計,システム設計及び一般)
- 誤差を有するシステムのシミュレーション結果に対する統計的解析とそのハードウェアによる高速化(設計環境,システム設計及び一般)
- プログラム可能な素子を利用したゲートレベル回路のデバッグ手法
- プログラム可能な素子を利用した大規模回路の自動修復手法