ZBDDを用いた検証方式におけるpartial order reductionの適用について
スポンサーリンク
概要
- 論文の詳細を見る
回路や仕様をモデル化して状態探索を行なう設計検証が一般的に広く実践されている.しかし, 大規模化し複雑化した回路においては, 状態数が爆発的に増大する傾向にある.そこで, 状態爆発を抑制する手法として, BDDなどを用いてシンボリックに状態探索を行う手法や, 検証に必要のない状態生成を抑え, 選択的な状態生成を行なうことで状態数を削減するpartial order reductionを用いた手法が提案されている.本報告では, 回路や仕様をペトリネットでモデル化することを前提に, 検証問題として単一プレースゼロ可達問題を取り上げ, これらの2つの手法を組み合せて, ZBDDに基づくシンボリックな状態探索のうえでpartial order reductionを実現するアルゴリズムを提案する.また, 提案する手法を実践し, 簡単な実験を行った結果を報告する.
- 社団法人電子情報通信学会の論文
- 1998-02-13
著者
-
米田 友洋
国立情報学研究所
-
米田 友洋
東京工業大学大学院情報理工学研究科計算工学専攻
-
米田 友洋
国立情報学研究所アーキテクチャ科学研究系
-
富坂 稔
東京工業大学大学院情報理工学研究科計算工学専攻
関連論文
- 高信頼オンチップ非同期データ転送技術に関する一検討(高信頼化,2009年並列/分散/協調処理に関する『仙台』サマー・ワークショップ(SWoPP仙台2009))
- AI-1-9 ディペンダブルNOCへの挑戦(AI-1.デイベンダブルVLSIに向けて,依頼シンポジウム,ソサイエティ企画)
- 束データ方式による非同期式回路の動作合成手法の提案(デザインガアイ2006-VLSI設計の新しい大地を考える研究会)
- 束データ方式による非同期式回路の動作合成手法の提案(動作合成/データパス合成,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 非同期式計算に基づくディペンダビリティ向上へのアプローチ(ディペンダブルコンピューティングシステム及び一般)
- 多値非同期式回路の形式的検証に関する研究
- 非同期式回路に基づく耐劣化故障性実現に関する考察(ディペンダブルコンピューティングシステム及び一般)
- 非同期式回路に基づく耐劣化故障性実現に関する考察(ディペンダブルコンピューティングシステム及び一般)
- 非同期式回路のFPGA実現とその評価(回路・設計手法)
- プロセス代数に基づく非同期式論理回路の設計検証 (非同期式回路/システム設計論文小特集)
- 空調制御ネットワークにおける信号極性確定の分散アルゴリズム
- FPGA実装を想定した束データ方式による非同期式回路のフロアプラン手法の検討
- 束データ方式による非同期式回路の動作合成手法の提案(動作合成/データパス合成,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 仕様記述言語Balsaからの非同期式回路合成について(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会)
- 仕様記述言語Balsaからの非同期式回路合成について(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 仕様記述言語Balsaからの非同期式回路合成について(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 仕様記述言語Balsaからの非同期式回路合成について(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 非同期式回路自動合成の高速化について(VLSIの設計/検証/テスト及び一般 論理合成及び高位合成)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-)
- 非同期式計算に基づくディペンダビリティ向上へのアプローチ(ディペンダブルコンピューティングシステム及び一般)
- FPGA実装を想定した束データ方式による非同期式回路のフロアプラン手法の検討 (ディペンダブルコンピューティング)
- FPGA実装を想定した束データ方式による非同期式回路のフロアプラン手法の検討 (VLSI設計技術)
- 8項 非同期式回路設計技術の現状(4節 通研講演会,第5章 国際会議・シンポジウム等)
- 高並列度仕様からの非同期式回路合成のための信号遷移挿入手法(論理合成,システムLSI設計とその技術)
- 高位仕様記述からの非同期式回路自動合成について(ハードウェア,フォーマルアプローチ論文)
- 時間付き信号遷移グラフの効率的縮約について(VLSIの設計/検証/テスト及び一般(デザインガイア))
- 時間付き信号遷移グラフの効率的縮約について(VLSIの設計/検証/テスト及び一般(デザインガイア))
- 時間付き信号遷移グラフの効率的縮約について(VLSIの設計/検証/テスト及び一般(デザインガイア))
- 時間付き信号遷移グラフの効率的縮約について(VLSIの設計/検証/テスト及び一般(デザインガイア))
- 資源制約に基づく高位非同期式回路仕様の変換について(ディペンダブルコンピュータシステム及び一般)
- 資源制約に基づく高位非同期式回路仕様の変換について(ディペンダブルコンピュータシステム及び一般)
- Force-Directed Scheduling アルゴリズムを用いた非同期式データパス回路合成と効率化の検討
- Force-Directed Schedulingアルゴリズムを用いた非同期式データパス回路合成と効率化の検討(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会)
- Force-Directed Schedulingアルゴリズムを用いた非同期式データパス回路合成と効率化の検討(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- Force-Directed Schedulingアルゴリズムを用いた非同期式データパス回路合成と効率化の検討(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- Force-Directed Schedulingアルゴリズムを用いた非同期式データパス回路合成と効率化の検討(論理合成+高位合成)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 非同期式回路の検証におけるIivenessクラスに関する考察
- 非同期式回路の検証におけるlivenessクラスに関する考察
- ハードウェアによるZBDD処理の実現に関する研究
- ハードウェアによるZBDD処理の実現に関する研究
- ハードウェアによるZBDD処理の実現に関する研究
- Net Unfoldingによるタイムペトリネットの効率的解析
- 有限遅延幅モデルにおける非同期式回路の検証について (テストと設計検証論文特集)
- 時間トレース理論に基づく非同期式回路の検証について
- Failure trace解析に基づくGasP回路の形式的検証
- 星状抽象ペトリネットの解析に関する研究
- 星状抽象ペトリネットの解析に関する研究
- 星状抽象ペトリネットの解析に関する研究
- ZBDDとpartial order reductionに基づく非同期式回路検証方式について
- ゼロサプレスBDDによるペトリネットのCTL記号モデル検査
- 非同期式回路検証のためのレベル指向モデルとその効率的解析法について
- 非同期式回路検証のためのレベル指向モデルとその効率的解析法について
- データパスを含む非同期式回路の検証について
- ZBDDに基づく非同期式回路の検証方式
- ZBDDを用いた検証方式におけるpartial order reductionの適用について
- 高速タイミング検証方式の実現とその効率評価
- ZBDDに基づく非同期回路の検証方式
- 非同期式回路検証器における使用記憶域削減について
- 非同期式回路検証器における使用記憶域削減について
- 非同期式回路検証器における使用記憶域削減について
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- Implementing Fast Boolean QDI Function Blocks
- Implementing Fast Boolean QDI Function Blocks
- Implementing Fast Boolean QDI Function Blocks
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- n 安全タイムペトリネットの発火規則について
- n安全タイムペトリネットの発火規則について
- ステートチャートのシンボリックな検証方式について
- シミュレーションを利用した形式的検証システム
- シミュレーションを利用した形式的検証システム
- 論理シミュレーションに基づくプロセッサの自動検証
- タイムペトリネットにおけるCTL記号モデル検査法について
- タイムペトリネットにおけるCTL記号モデル検査法について
- 非同期式回路自動合成の高速化について(VLSIの設計/検証/テスト及び一般 論理合成及び高位合成)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-)
- 非同期式回路の高位合成について(デペンダブルコンピュータシステム及び一般)
- 非同期式回路の高位合成について(ディペンダブルコンピュータシステム及び一般)
- Partial Order Reductionに基づくTimed回路のsafety/timing failure検出アルゴリズムの効率化について
- 対称性及び抽象化を利用した検証方式の効率化 (テストと設計検証論文特集)
- 正規表現を利用したスケーラブル環状回路の検証
- 正規表現を利用したスケーラブル環状回路の検証
- 対称性及び抽象化を利用した検証方式の効率化
- 非同期式回路自動合成の高速化について(VLSIの設計/検証/テスト及び一般論理合成及び高位合成)
- 整数線形計画問題に基づいたネットワークオンチップにおけるフォールトトレランスのためのタスクの多重割り当て手法(微細化対応技術,デザインガイア2011-VLSI設計の新しい大地-)
- 整数線形計画問題に基づいたネットワークオンチップにおけるフォールトトレランスのためのタスクの多重割り当て手法(微細化対応技術,デザインガイア2011-VLSI設計の新しい大地-)
- 整数線形計画問題に基づいたネットワークオンチップにおけるフォールトトレランスのためのタスクの多重割り当て手法
- 整数線形計画問題に基づいたネットワークオンチップにおけるフォールトトレランスのためのタスクの多重割り当て手法
- 非同期式回路自動合成の高速化について(VLSIの設計/検証/テスト及び一般 論理合成及び高位合成)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-)
- 有限幅遅延モデルに基づく非同期式回路検証方式とその効率化(ペトリネットの応用特集号)
- ディペンダブルネットワークオンチッププラットフォームによる車載制御の実証に向けて
- ディペンダブルネットワークオンチッププラットフォームによる車載制御の実証に向けて
- ディペンダブルネットワークオンチッププラットフォームによる車載制御の実証に向けて(ディペンダブルシステム,組込み技術とネットワークに関するワークショップETNET2013)
- ディペンダブルネットワークオンチッププラットフォームによる車載制御の実証に向けて(ディペンダブルシステム,組込み技術とネットワークに関するワークショップETNET2013)
- 7.3 非同期式ネットワークオンチップ(第7章:時間応答性,ディペンダブルVLSIシステム)
- 10.5 多重化CPUコアの故障検出と再構成手法(第10章:将来の課題,ディペンダブルVLSIシステム)
- 高信頼なネットワークオンチップ実現のためのマルチタスクのスケジューリングとアロケーション(上流設計,システムオンシリコンを支える設計技術)
- 2相ハンドシェイクプロトコル非同期式回路向けマルチクロック・マルチエッジトリガ・フリップフロップの提案(システムLSIの応用とその要素技術,専用プロセッサ,プロセッサ,DSP,画像処理技術,及び一般)
- 2相ハンドシェイクプロトコル非同期式回路向けマルチクロック・マルチエッジトリガ・フリップフロップの提案(システムLSIの応用とその要素技術,専用プロセッサ,プロセッサ,DSP,画像処理技術,及び一般)