CPU設計導入教育への形式的設計検証手法の適用

情報処理学会 HANDLE Web Site 参考文献13件 オープンアクセス

書誌事項

タイトル別名
  • CPU　セッケイ　ドウニュウ　キョウイク　ヘノ　ケイシキテキ　セッケイ　ケンショウ　シュホウ　ノ　テキヨウ
  • CPU セッケイ ドウニュウ キョウイク エ ノ ケイシキテキ セッケイ ケンショウ シュホウ ノ テキヨウ
  • Applying Formal Verification Method to Education in Design of CPU
  • 設計技術と設計自動化

この論文をさがす

抄録

形式的手法の設計導入教育への適用の有用性を調べるために，大阪大学基礎工学部情報科学科3年次学生のCPU設計実験において，(i)我々の研究グループで作成した検証システムを用いて設計の正しさを形式的に証明する設計手法（新手法），(ii)慎重な見直しや波形シミュレーションなどで設計の正しさを確認する設計手法（従来手法），の2つのコースを設けて，その2つのコース間で作業時間と設計したCPUにおける誤りの有無について2カ年にわたって比較を行った．定められた中間レポート提出期限までに誤りのないCPUを設計した学生は，従来手法コースでは42人中0人，新手法コースでは42人中41人であった．従来手法コースでは提出期限後に，教官が誤りを指摘して学生が設計を修正する期間を設け，この期間に19人が誤りのないCPUを設計した．中間レポート提出期限までに費やした全作業時間の平均は新手法43時間に比べて従来手法のほうが13時間ほど短かった．以上より，あらかじめ定められた期限までに正しいCPUを設計するためには，新手法は30%ほど作業時間がかかるものの効果的であることが確かめられた．

In order to compare a formal method with a conventional method for designing CPUs,we have measured several metrics (workload and the number of logical errors of the CPUs)for two years in CPU designing laboratory work for undergraduate students in Computer and Information Science at Osaka University.Here, eighty-four students were divided into two groups; Course V and Course T.Each student in Course V used our verifiers to prove the correctness of his/her design,while each student in Course T carefully observed the design or used a waveform simulator.Nobody (out of forty-two students) correctly designed CPUs in Course T by a deadline,while forty-one (out of forty-two) correctly designed CPUs in Course V by the same deadline.The average working time of Course T students elapsed by the deadline is 30 hours and it is 30% shorter than that of Course V students.From the comparison results,we can conclude that the formal method is useful for designing a CPU correctly within a pre-fixed period.

収録刊行物

参考文献 (13)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ