HDLで記述されたハードウェア設計の時相論理による検証
スポンサーリンク
概要
- 論文の詳細を見る
本稿では, ハードウェア記述言語(HDL)で記述されたハードウェアの仕様を, その記述から直接, 形式的手法を用いて検証する方法を提案する.対象とするHDLは, ハードウェア合成システムPARTHENONで用いられるHDL(SFLと呼ばれる)である.この方法の核となる部分は, SFLで記述されたハードウェアの動作の記述を, その状態遷移関係を表現するブール式に自動変換することである.このブール式が, 時相論理CTLのよく知られたモデルチェックアルゴリズムにかけられ, CTL式で表現されたハードウェアの性質が検証される.本稿では, モデルチェックアルゴリズムの検証の結果がSFLの動作セマンティクスに正確に対応するためには, SFLの各動作をどのように論理表現すればよいかを示す.
- 1999-01-11
著者
-
櫟 粛之
日本電信電話株式会社NTTコミュニケーション科学基礎研究所
-
澤田 宏
NTTコミュニケーション科学基礎研究所
-
澤田 宏
日本電信電話株式会社NTTコミュニケーション科学基礎研究所
-
櫟 粛之
NTTコミュニケーション科学基礎研究所
-
櫟 粛之
日本電信電話株式会社
関連論文
- Techniques to accelerate request processing for Byzantine fault tolerance (コンピュテーション)
- 周波数領域ブラインド音源分離のための極座標表示に基づく活性化関数
- 複数人会話における非言語インタラクション構造の推定--誰が誰にどのように反応しているか?
- UC frameworkにおけるfunctionalityの合成について(情報通信基礎サブソサイエティ合同研究会)
- 招待講演 時間周波数マスクによる実環境でのブラインド音源分離 (応用音響)
- 再構成可能なハードウェアを用いた充足可能性問題の解法
- しきい論理に基づく再構成可能デバイスの可変論理部
- しきい論理に基づく再構成可能デバイスの可変論理部
- しきい論理に基づく再構成可能デバイスの可変論理部
- ニューロンMOSによる対称関数回路の設計
- ニューロンMOSによる対称関数回路の設計手法
- ニューロンMOSを可変論理部に用いた再構成可能デバイスに関する検討
- ニューロンMOSによる対称関数回路の設計手法
- ニューロンMOSを可変論理部に用いた再構成可能デバイスに関する検討
- SPFD : 論理関数の自由度の新しい表現方法
- 論理関数の種々の分解手法を統合したLUT回路合成法
- 論理関数の種々の分解手法を統合したLUT回路合成法
- 論理関数の種々の分解手法を統合したLUT回路合成法
- 変数の重なりのない単純な関数分解を用いた組合せ回路の改善方法
- OWLオントロジー間の自動対応付け手法の提案と評価(「さまざまな分野の形式的検証最前線」及びAI一般)
- 音源分離技術の最新動向
- 多クラス早期認識ブースティング法(一般,顔・人物・ジェスチャ・行動)
- 多クラス早期認識ブースティング法(一般,顔・人物・ジェスチャ・行動)
- Byzantine Agreement on the Order of Processing Received Requests is Solvable Deterministically in Asynchronous Systems
- 音声区間推定と時間周波数領域方向推定の統合による会議音声話者識別(音響信号処理/一般)
- AS-4-5 音声のスパース性を用いたUnderdetermined音源分離(AS-4. ICAを超える,シンポジウムセッション)
- A-10-6 周波数領域ICAにおける初期値の短時間データからの学習(A-10. 応用音響,一般セッション)
- A-10-9 多くの背景音からの主要音源のブラインド抽出(A-10.応用音響,基礎・境界)
- A-10-8 3次元マイクロホンアレイを用いた多音源ブラインド分離(A-10.応用音響,基礎・境界)
- A-10-7 観測ベクトルのクラスタリングによるブラインド音源分離(A-10.応用音響,基礎・境界)
- 畳込み混合のブラインド音源分離(独立成分分析とその応用特集号)
- 周波数領域ICAと時間領域ICAを統合したSIMOモデル信号のブラインド抽出法の評価(マイクロホンアレー・ブラインド分離・音源位置推定/一般)
- ブラインド信号処理技術の研究動向(マイクロホンアレー・ブラインド分離・音源位置推定/一般)
- [招待論文]独立成分分析に基づくブラインド音源分離(マイクロホンアレー・ブラインド分離・音源位置推定及び一般)
- 移動音源の低遅延実時間ブラインド分離
- 周波数領域ブラインド音源分離における permutation 問題の頑健な解法
- 周波数領域ICAと時間遅れスペクトル減算による残響下での実時間ブラインド音源分離
- 間隔の異なる複数のマイクペアによるブラインド音源分離
- 非定常スペクトルサブトラクションによる音源分離後の残留雑音除去
- BDIアーキテクチャにおけるコミットメント戦略を実現するための形式的検証手続き(ソフトウェア基礎,プログラム理論)
- エージェントの相互信念を扱う拡張BDI logicの演繹体系
- 合理的エージェントの心的状態に関する整合性の実現と応用について(ソフトウェアエージェントとその応用論文)
- エージェントの相互信念を扱う拡張BDI logicの演繹体系
- BDI Logicのsequent calculusによる演繹体系(マルチエージェント)
- H-021 ファッション雑誌を用いたコーディネート推薦システム(H分野:画像認識・メディア理解,一般論文)
- F-056 ネットワーク構造による類似探索性能の分析法の提案(F分野:人工知能・ゲーム,一般論文)
- RF-007 オブジェクト集合に依存したRNGの特性分析(F分野:人工知能・ゲーム,査読付き論文)
- 確率的近似法を用いた頑強なオンライン評判メカニズム(分散協調とエージェント)
- エージェント間通信における信頼度計算手法
- モバイルエージェント実行計画問題について (計算機科学基礎理論とその応用)
- 負荷分散のための非同期分散分枝限定法
- Generic Communication Protocol Program を利用したエージェントの interoperability の実現
- 変数の重なりのない単純な関数分解を用いた組合せ回路の改善方法
- 論理関数の自由度の新しい表現方法とそのFPGA向け論理設計への応用
- 論理関数の自由度の新しい表現方法とそのFPGA向け論理設計への応用
- 対称変数の検出による関数分解の高速化と多段論理合成への応用
- UC frameworkにおけるfunctionalityの合成について(情報通信基礎サブソサイエティ合同研究会)
- UC frameworkにおけるfunctionalityの合成について(情報通信基礎サブソサイエティ合同研究会)
- DS-1-1 汎用的結合性のある秘密多項式評価法(DS-1. COMP-NHC学生シンポジウム,シンポジウムセッション)
- 形式的検証機能を備えたインターネットエージェントプログラミングシステム
- インターネットエージェントのための動的スナップショットアルゴリズムと部分ロールバックアルゴリズム(分散協調とエージェント)
- インターネットエージェントの非同期な資源取引における無待機アルゴリズム
- インターネットエージェントのための動的スナップショットアルゴリズムと部分ロールバックアルゴリズム
- 鍵交換プロトコルのFunctionality合成について(「さまざまな分野の形式的検証最前線」及びAI一般)
- 鍵交換プロトコルの Functionality 合成について
- インターネットエージェントシステムのための実用的な耐ビザンチン故障方式(セッション1)
- 形式的検証機能を備えたインターネットエージェントプログラミングシステム(セッション1)
- 時間周波数マスクによる実環境でのブラインド音源分離
- Task-PIOAに基づくIdeal Functionality実現の証明の自動化(「さまざまな分野の形式的検証最前線」及びAI一般)
- インターネットエージェントとその基礎理論(「21世紀の知識情報科学に向けて」,及び一般)
- エージェントプログラミングとその形式的検証
- 知識と信念の推論に基づくモバイルエージェントシステム
- HDLで記述されたハードウェア設計の時相論理による検証
- HDLで記述されたハードウェア設計の時相論理による検証
- First-Order定義可能な様相命題論理体系に対する自動定理証明
- 停止性を保証する汎用様相論理定理証明手続き
- デフォルト論理に基づく知識プログラミングシステムとそのプログラム変換の理論的枠組み
- A-10-9 フルランク空間相関行列モデルに基づく拡散性雑音除去(A-10.応用音響,一般セッション)
- 非負値行列因子分解NMFの基礎とデータ/信号解析への応用
- Latent Dirichlet Allocationを用いた潜在的構造変化検知(ベイズ統計モデル,統計推理,データベース,一般)
- 非負制約下における複合行列分解
- サブセット無限関係モデル(第15回情報論的学習理論ワークショップ)
- sNMF:非負値制約下における複数行列の同時分解法 : ソーシャルメディア解析を応用例として(第15回情報論的学習理論ワークショップ)
- 線形回帰モデルにおけるNCスペクトラルクラスタリングを用いた効率的な入力変数選択(第15回情報論的学習理論ワークショップ)