@techreport{oai:ipsj.ixsq.nii.ac.jp:00091729,
 author = {山田, 雄二 and 富岡, 涼太 and 高橋, 隆一 and Yuji, Yamada and Ryota, Tomioka and Ryuichi, Takahashi},
 issue = {6},
 month = {May},
 note = {設計の大規模化や複雑化に伴い検証とテストが重要な課題となっている．本研究ではテストパターンに依存せずに網羅的な検証が行える形式的検証に注目した．形式的検証には定理証明型とモデル検査がある．定理証明型では設計が満たすべき定理を実際の設計が満たしている公理から導けるか調べることで検証を行う．定理と公理の記述は定理証明に用いる処理系の制約を受ける．モデル検査では設計をクリプキ構造で表し，設計が満たすべき性質をCTLで記述して検証を行う．状態数が多くなるという問題がある．本研究では定理と公理の両者をCTL式で表し，CTL演繹体系を用いて公理から定理を導くことによる検証を試みた．簡単な4段パイプライン・コンピュータを設計して，パイプライン化で問題になるハザードを検証対象とした．, 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.},
 title = {マイクロアーキテクチャのCTL演繹体系を用いた検証},
 year = {2013}
}