準形式的モデル検査のハードウェア実装による高速化の検討(モデル・回路,組込技術とネットワークに関するワークショップETNET2008)
スポンサーリンク
概要
- 論文の詳細を見る
近年設計が大規模になり、複雑化が進むにつれて検証の重要性が増している。現在の重要な検証手法の一つであるモデル検査には適用する回路規模が大きくなると状態爆発を起こし、実用的な時間内で検査が終了しないという問題がある。そのため回路規模や検証時間の面でより効率的なモデル検査が必要とされている。現在の効率的なモデル検査手法の1つに、コンパイルドシミュレーションを基にした準形式的限定モデル検査がある。本稿ではそのアルゴリズムの一部をハードウェアで実装し、各々の処理に対してハードウェア・ソフトウェア協調実行に向けた最適化を行うことで高速化したモデル検査を提案する。また例題を用いた実験によって実際に高速に検証を行い、提案手法の有効性を確認した。
- 2008-03-27
著者
-
藤田 昌宏
東京大学大学院工学系研究科電子工学
-
森下 賢志
東京大学工学部電子工学科
-
藤田 昌宏
東京大学大規模集積システム設計教育研究センター:科学技術振興機構戦略的創造研究推進事業crest
-
吉田 浩章
東京大学大学院工学系研究科
-
吉田 浩章
東京大学大規模集積システム設計教育研究センター(vdec)|科学技術振興機構戦略的創造研究推進事業crest
関連論文
- A method of reproducing input/output error trace on high-level design for hardware debug support (ディペンダブルコンピューティング)
- TA-1-3 高位検証技術の基礎
- 「システムLSIの設計技術と設計自動化」の編集にあたって
- 算術演算回路のデバッグ支援技術
- SpecC言語に基づくシステムレベル設計手法
- LSIの設計品質はCADツールの使いこなしが決める! : CAD技術の研究開発なくして高性能LSIはない
- 問題点のまとめと1つの提案
- システムLSIの設計技術・設計支援技術(CAD技術)に関する問題点
- 設計再利用のためのIPライブラリ検索システム(上流設計技術(1),システムオンシリコン設計技術並びにこれを活用したVLSI)
- SATアルゴリズムの最新動向
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバック,組込技術とネットワークに関するワークショップETNET2009)
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバッグ,組込技術とネットワークに関するワークショップETNET2009)
- 専用プロセッサ用命令セットの自動生成手法の提案と実装
- ハードウェアデバッグ支援のためのエラー入出力トレースの上位レベル設計における再現手法(高位レベルテスト・検証,VLSI設計とテスト及び一般)
- 準形式的モデル検査のハードウェア実装による高速化の検討(モデル・回路,組込技術とネットワークに関するワークショップETNET2008)
- 算術演算回路のデバッグ支援技術
- SpecC言語に基づくシステムレベル設計手法
- SpecC言語に基づくシステムレベル設計手法
- Performance-Constrained Transistor Sizing for Different Cell Count Minimization
- AI-1-4 超ディペンダブルVLSIへの挑戦(AI-1.デイベンダブルVLSIに向けて,依頼シンポジウム,ソサイエティ企画)
- 製造後デバッグのための入出力シーケンススライシング手法(設計/テスト/検証)
- Synchronization Verification in System-Level Design with ILP Solvers(System Level Design,VLSI Design and CAD Algorithms)
- 電子系・機械系協調設計における設計検証法に関する検討(実時間処理,組込システム及び一般)
- 電子系・機械系協調設計における設計検証法に関する検討(実時間処理,組込システム及び一般)
- 充足可能性判定に基づくシステムレベルデバッグ支援手法におけるバグモデルの導入による効率化
- 上位設計記述の解析を利用した製造後機能テストの効率化
- 動的パッチ読み出し機構を備えた製造後機能修正可能アクセラレータ
- EFSM-based Weight-oriented Concolic Testing for Embedded Software
- 依存グラフを用いた局所的な記号シミュレーションによるC言語記述に対する等価性検証手法の提案(システムLSI設計及び一般)
- 依存グラフを用いた局所的な記号シミュレーションによるC言語記述に対する等価性検証手法の提案(システムLSI設計及び一般)
- C言語を対象とした記述間の差異に基づく効率的な等価性検証手法(システムオンシリコン設計技術並びにこれを活用したVLSI)
- C言語を対象とした記述間の差異に基づく効率的な等価性検証手法(システムオンシリコン設計技術並びにこれを活用したVLSI)
- C言語でのハードウェア記述に対する効率的な等価性検証手法の提案(システム設計及び一般)
- C言語でのハードウェア記述に対する効率的な等価性検証手法の提案(システム設計及び一般)
- ループ融合を利用した複数のforループからのパイプラインハードウェア合成
- ループ融合を利用した複数の for ループからのパイプラインハードウェア合成
- システムレベル設計記述に対する具体値・記号値シミュレーションによる入力パターンの自動生成手法(SoC・解析,組込技術とネットワークに関するワークショップETNET2008)
- システムレベル設計記述に対する具体値・記号値シミュレーションによる入力パターンの自動生成手法(SoC・解析,組込技術とネットワークに関するワークショップETNET2008)
- システムレベル設計記述に対する具体値・記号値シミュレーションによる入力パターンの自動生成手法(SoC・解析,組込技術とネットワークに関するワークショップETNET2008)
- システムレベル設計記述に対する具体値・記号値シミュレーションによる入力パターンの自動生成手法(SoC・解析,組込技術とネットワークに関するワークショップETNET2008)
- 1M-5 ワードレベル論理式の充足可能性判定問題を利用したシステムレベル設計デバッグ支援手法(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 設計固有セルライブラリの自動生成手法(論理設計,デザインガイア2009-VLSI設計の新しい大地)
- Increasing yield using partially-programmable circuits (VLSI設計技術)
- 設計固有セルライブラリの自動生成手法(論理設計,デザインガイア2009-VLSI設計の新しい大地-)
- Increasing yield using partially-programmable circuits (ディペンダブルコンピューティング)
- チップ内プログラマブル配線向け形式的検証手法(暗号処理回路,システムオンシリコンを支える設計技術)
- リンク長及びレイテンシ制約下でのネットワークオンチップのトポロジ自動生成(ネットワークオンチップ,システムオンシリコンを支える設計技術)
- 内部等価点の推定によるルールベース高位検証の高精度化(高位検証,デザインガイア2008-VLSI設計の新しい大地)
- 反例を利用した網羅性の高いプロパティ集合生成手法(高位検証,デザインガイア2008-VLSI設計の新しい大地)
- メモリアクセスおよびリソース共有を行うカスタム命令自動生成手法(FPGA・低消費電力設計・システムレベル合成,システム設計及び一般)
- メモリアクセスおよびリソース共有を行うカスタム命令自動生成手法(FPGA・低消費電力設計・システムレベル合成,システム設計及び一般)
- 充足可能性判定を利用した最適コード生成手法
- 反例を利用した網羅性の高いプロパティ集合生成手法(高位検証,デザインガイア2008-VLSI設計の新しい大地)
- 反例を利用した網羅性の高いプロパティ集合生成手法(高位検証,デザインガイア2008-VLSI設計の新しい大地-)
- 既存設計の再利用を考慮したSoCの仕様記述手法と上位設計方法論
- ハードウェア設計における設計資産の仕様記述およびその検証手法(上流設計技術(1),システムオンシリコン設計技術並びにこれを活用したVLSI)
- 設計再利用のためのIPライブラリ検索システム(上流設計技術(1),システムオンシリコン設計技術並びにこれを活用したVLSI)
- ハードウェア設計における設計資産の仕様記述およびその検証手法(上流設計技術(1),システムオンシリコン設計技術並びにこれを活用したVLSI)
- プロトコル表現効率化に基づくプロトコル変換器合成手法に関する研究(組込技術とネットワークに関するワークショップETNET2006)
- プロトコル表現効率化に基づくプロトコル変換器合成手法に関する研究(組込技術とネットワークに関するワークショップETNET2006)
- プロトコル表現効率化に基づくプロトコル変換器合成手法に関する研究(組込技術とネットワークに関するワークショップETNET2006)
- 分割二分決定グラフによる有限状態機械の到達可能性解析の PC クラスタを用いた並列実装手法の提案(設計技術と設計自動化)(情報システム論文)
- 分割二分決定グラフによる有限状態機械の到達可能性解析のPCクラスタを用いた並列実装手法の提案
- 仮想マルチプロセッサモデルに基づく高速SoCプロトタイピング手法(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 仮想マルチプロセッサモデルに基づく高速SoCプロトタイピング手法(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 高性能SoCプロトタイプのFPGA実装方式の検討(論理設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 高性能SoCプロトタイプのFPGA実装方式の検討(論理設計1,デザインガイア2010-VLSI設計の新しい大地-)
- システムレベル設計における並列動作の同期に関するデバッグ支援手法(デバック,組込技術とネットワークに関するワークショップETNET2009)
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバック,組込技術とネットワークに関するワークショップETNET2009)
- システムレベル設計における並列動作の同期に関するデバッグ支援手法(デバック,組込技術とネットワークに関するワークショップETNET2009)
- システムレベル設計における並列動作の同期に関するデバッグ支援手法(デバッグ,組込技術とネットワークに関するワークショップETNET2009)
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバッグ,組込技術とネットワークに関するワークショップETNET2009)
- システムレベル設計における並列動作の同期に関するデバッグ支援手法(デバッグ,組込技術とネットワークに関するワークショップETNET2009)
- 順序回路の上位設計記述における等価性指定の自動化手法(高位検証,FPGA応用及び一般)
- 仕様から自動生成されたプロパティによるプロトコル変換機の形式的検証手法(高位検証,FPGA応用及び一般)
- 仕様から自動生成されたプロパティによるプロトコル変換機の形式的検証手法(高位検証,FPGA応用及び一般)
- 順序回路の上位設計記述における等価性指定の自動化手法(高位検証,FPGA応用及び一般)
- 順序回路の上位設計記述における等価性指定の自動化手法(高位検証,FPGA応用及び一般)
- 積グラフ探索を利用した実用的なプロトコル変換器の自動合成と検証(システムオンシリコン設計技術並びにこれを活用したVLSI)
- 積グラフ探索を利用した実用的なプロトコル変換器の自動合成と検証(システムオンシリコン設計技術並びにこれを活用したVLSI)
- IP再利用のための動的再構成可能プロトコル変換器合成手法(設計・最適化技術)
- 動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討(検証・シミュレーション,システム設計及び一般)
- 動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討(検証・シミュレーション,システム設計及び一般)
- 動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討
- 状態遷移表現への変換に基づくハードウェア/ソフトウェア協調設計の形式的検証手法(ハードウェア,フォーマルアプローチ論文)
- 組込みシステムのシステムレベル設計におけるオブジェクト指向技術の応用(組込技術とネットワークに関するワークショップETNET2006)
- 組込みシステムのシステムレベル設計におけるオブジェクト指向技術の応用(組込技術とネットワークに関するワークショップETNET2006)
- 組込みシステムのシステムレベル設計におけるオブジェクト指向技術の応用(組込技術とネットワークに関するワークショップETNET2006)
- FSMへの変換に基づくHW/SW協調設計の形式的検証手法に関する研究(設計・合成, 組込技術とネットワークに関するワークショップ)
- FSMへの変換に基づくHW/SW協調設計の形式的検証手法に関する研究
- FSM への変換に基づく HW/SW 協調設計の形式的検証手法に関する研究(設計・合成, 組込技術とネットワークに関するワークショップ)
- トランスダクション法を用いた非同期制御回路最適化
- 時相論理によるハードウェア同期部の仕様記述とPrologによるその状態遷移表への自動合成法
- ハードウェア状態遷移表現のPrologによる検証
- 時相論理によるハードウェア仕様記述とPrologを用いたゲート回路の検証
- C. Mead and L. Conway, Introduction to VLSI Systems, Addison-Wesley, 1980(20世紀の名著名論)
- 1M-6 動作合成された束データ方式による非同期式回路とその動作仕様に対する等価性検証手法(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 2P-1 動的ウェブアプリケーションの操作に対する画面間遷移の網羅的検証(ソフトウェアの検査・検証,学生セッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- システムレベル設計言語に対するフォールスパスを考慮した性能評価(システムオンシリコン設計技術並びにこれを活用したVLSI)
- システムレベル設計言語に対するフォールスパスを考慮した性能評価(システムオンシリコン設計技術並びにこれを活用したVLSI)