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

北浜, 優子; 北嶋, 曉; 岡野, 浩三 他

情報処理学会論文誌, 2000, 41(11), 3114-3121

アクセス数:448件（2025-04-27 10:40 集計）

固定URL: https://hdl.handle.net/11094/50250

閲覧可能ファイル 

ファイル フォーマット 利用条件 サイズ 閲覧回数 利用開始日 説明 information
ipij-jnl_41_11_3114 pdf なし 289 KB 403 2014.10.01 出版社版/publisher  

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル
CPU設計導入教育への形式的設計検証手法の適用
Applying Formal Verification Method to Education in Design of CPU
CPU　セッケイ　ドウニュウ　キョウイク　ヘノ　ケイシキテキ　セッケイ　ケンショウ　シュホウ　ノ　テキヨウ
著者
著者名
北浜, 優子 ; キタハマ, ユウコ ; Kitahama, Yuko
NRID
1000000304030 1000000304030
著者名
北嶋, 曉 ; キタジマ, アキラ ; Kitajima, Akira
NRID
1000070252632 1000070252632
著者名
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000000029513 1000000029513
著者名
谷口, 健一 ; タニグチ, ケンイチ ; Taniguchi, Kenichi
抄録
形式的手法の設計導入教育への適用の有用性を調べるために，大阪大学基礎工学部情報科学科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.
出版者
情報処理学会
ジョウホウ　ショリ　ガッカイ
収録物名
情報処理学会論文誌
巻(号)
41(11)
ページ
3114-3121
刊行年月
2000-11-15
言語
日本語
ハンドルURL
https://hdl.handle.net/11094/50250
PISSN
03875806
NCID
AN00116647
アクセス権
open access
権利情報
ここに掲載した著作物の利用に関する注意 本著作物の著作権は情報処理学会に帰属します。本著作物は著作権者である情報処理学会の許可のもとに掲載するものです。ご利用に当たっては「著作権法」ならびに「情報処理学会倫理綱領」に従うことをお願いいたします。
Notice for the use of this material The copyright of this material is retained by the Information Processing Society of Japan (IPSJ). This material is published on this web site with the agreement of the author (s) and the IPSJ. Please be complied with Copyright Law of Japan and the Code of Ethics of the IPSJ if any users wish to reproduce, make derivative work, distribute or make available to the public any part or whole thereof. All Rights Reserved, Copyright (C) Information Processing Society of Japan. Comments are welcome. Mail to address editj＠ipsj.or.jp, please.
出版タイプ
Version of Record
カテゴリ
学術雑誌論文 Journal Article