CPUの高位設計において，段階的詳細化の正しさの証明に
形式的手法を用いること，および，証明を自動化するこ
とは有用であると考えられる．昨年度の本学3年次学生の
CPU設計実験において，設計するCPU用の自動検証ツール
を用いた新手法を導入し，波形シミュレーションによっ
て正しさを確認する従来手法と比較した．その結果，設
計作業の効率化において新手法が有用であるという見通
しを得た．また，新手法の導入によって学生の形式的手
法に対する理解を深める効果があることもわかった．
そこで，本年度の学生実験にも新手法を導入し，できあ
がったCPUの信頼性についても比較を行う．本発表では，
これらの比較方法，実験計画などについて述べる．
Back