マイクロアーキテクチャのCTL演繹体系を用いた検証
スポンサーリンク
概要
- 論文の詳細を見る
設計の大規模化や複雑化に伴い検証とテストが重要な課題となっている.本研究ではテストパターンに依存せずに網羅的な検証が行える形式的検証に注目した.形式的検証には定理証明型とモデル検査がある.定理証明型では設計が満たすべき定理を実際の設計が満たしている公理から導けるか調べることで検証を行う.定理と公理の記述は定理証明に用いる処理系の制約を受ける.モデル検査では設計をクリプキ構造で表し,設計が満たすべき性質をCTLで記述して検証を行う.状態数が多くなるという問題がある.本研究では定理と公理の両者をCTL式で表し,CTL演繹体系を用いて公理から定理を導くことによる検証を試みた.簡単な4段パイプライン・コンピュータを設計して,パイプライン化で問題になるハザードを検証対象とした.
- 2013-05-09
著者
関連論文
- 正規直交展開を用いた論理回路のテスト容易性に関する一考察
- 冗長論理回路のテスタビリティ評価尺度に関する一考察(ディペンダブルコンピュータシステム及び一般)
- マルチレートフィルタと帯域制限補間を用いたウェーブレット変換による楽音モーフィング
- マルチレートフィルタを用いたウェーブレット変換による感性情報処理 : 民族音楽と生理指標解析のための一手法
- 2H-10 データ駆動型ノイマンマシン(DDNM)の構築 : 各プログラムモジュールのクリティカルパスでの処理速度を目指して
- 2H-9 データ駆動型ノイマンマシン(DDNM)におけるスケジューリング : SPECint95ベンチマークテストの試み
- システムのインテリジェント化を支えるディジタル設計教育(新しい知能化へ向けたLSIシステム技術)
- ウェーヴレット変換を用いた心拍データの解析 : 音楽鑑賞によるリラクセーションを求めて
- ノイマン型コンピュータのデータ駆動型マシン技術を用いた高速化 : モジュールフェッチを前提とするループ・アンローリングのハードウエアによる実現
- ウェーヴレット変換のためのスケーラブルなデータ駆動型マシンの一構成法
- 完全なインターロックを行なうパイプラインCISC/RISCの設計教育 : マイクロコンピュータ設計教育環境City-1の2年目
- 完全なインターロックを行なうパイプラインCISC/RISCの設計教育 : マイクロコンピュータ設計教育環境City-1の2年目
- マイクロコンピュータ設計教育環境City-1 : FPGAコンピュータの自由な設計と製作
- FPGAを用いたスーパースカラ設計教育に関する一考察
- 状況に埋め込まれた細粒度マイクロコンピュータ設計教育
- 冗長論理回路のテスタビリテイ評価尺度に関する一考察(ディペンダブルコンピュータシステム及び一般)
- マイクロアーキテクチャのCTL演繹体系を用いた検証
- マイクロアーキテクチャのCTL演繹体系を用いた検証 (VLSI設計技術)
- マイクロアーキテクチャのCTL演繹体系を用いた検証(検証・デバック技術,システム設計及び一般)