マイクロアーキテクチャのCTL演繹体系を用いた検証

• Item type: SIG Technical Reports(1)
• 公開日: 2013-05-09
• タイトル: マイクロアーキテクチャのCTL演繹体系を用いた検証
• タイトル / 言語: en
• タイトル: Microarchitecture Verification using CTL Deduction system
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 検証・デバック技術
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 広島市立大学情報科学研究科情報工学専攻
• 著者所属: 広島市立大学情報科学研究科情報工学専攻
• 著者所属: 広島市立大学情報科学研究科情報工学専攻
• 著者所属(英): en
• 著者所属(英): Faculty of Information Sciences, Hiroshima City University
• 著者所属(英): en
• 著者所属(英): Faculty of Information Sciences, Hiroshima City University
• 著者所属(英): en
• 著者所属(英): Faculty of Information Sciences, Hiroshima City University
• 著者名: 山田, 雄二; 富岡, 涼太; 高橋, 隆一
• 著者名(英): Yuji, Yamada; Ryota, Tomioka; Ryuichi, Takahashi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 設計の大規模化や複雑化に伴い検証とテストが重要な課題となっている．本研究ではテストパターンに依存せずに網羅的な検証が行える形式的検証に注目した．形式的検証には定理証明型とモデル検査がある．定理証明型では設計が満たすべき定理を実際の設計が満たしている公理から導けるか調べることで検証を行う．定理と公理の記述は定理証明に用いる処理系の制約を受ける．モデル検査では設計をクリプキ構造で表し，設計が満たすべき性質をCTLで記述して検証を行う．状態数が多くなるという問題がある．本研究では定理と公理の両者をCTL式で表し，CTL演繹体系を用いて公理から定理を導くことによる検証を試みた．簡単な4段パイプライン・コンピュータを設計して，パイプライン化で問題になるハザードを検証対象とした．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Verification and test have become critically important as the scale of the design grows. This paper investigates the formal verification which could be done without using the test patterns. Theorem proving method and the model checking are two prior methods for the formal verification. In the theorem proving method, the verification is accomplished by trying to prove the theorem, which should be satisfied in the design, by using the axioms which represent the implementation. The description style for the theorems and the axioms depend on the theorem prover available. In the model checking, designs are expressed in the Kripke structure, which is used to verify the properties in CTL, which are expected to be satisfied on the structure. The number of the states tends to become too many. In this paper, we tried to express the design in CTL and tried to deduct the properties in CTL by using CTL deduction system. We investigated the hazards on a small scale pipelined computer having 4 stages.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 研究報告システムLSI設計技術（SLDM）; 巻 2013-SLDM-161, 号 6, p. 1-6, 発行日 2013-05-09
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会