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

北浜, 優子; キタハマ, ユウコ; Kitahama, Yuko; 北嶋, 曉; キタジマ, アキラ; Kitajima, Akira; 岡野, 浩三; オカノ, コウゾウ; Okano, Kozo; 谷口, 健一; タニグチ, ケンイチ; Taniguchi, Kenichi

アクセス数:358件（2024-04-23 22:25 集計）

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

閲覧可能ファイル

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

論文情報

ファイル出力

タイトル	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

資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
DCMI資源タイプ	text
DCTERMS.bibliographicCitation	情報処理学会論文誌. 2000, 41(11), p. 3114-3121
DC.title	CPU設計導入教育への形式的設計検証手法の適用
	Applying Formal Verification Method to Education in Design of CPU
	CPU　セッケイ　ドウニュウ　キョウイク　ヘノ　ケイシキテキ　セッケイ　ケンショウ　シュホウ　ノ　テキヨウ
DC.creator	北浜, 優子
	キタハマ, ユウコ
	Kitahama, Yuko
	北嶋, 曉
	キタジマ, アキラ
	Kitajima, Akira
	岡野, 浩三
	オカノ, コウゾウ
	Okano, Kozo
	谷口, 健一
	タニグチ, ケンイチ
	Taniguchi, Kenichi
DC.publisher	情報処理学会
DC.publisher	ジョウホウ　ショリ　ガッカイ
DC.language' scheme='DCTERMS.RFC1766	日本語
DC.type' scheme='DCTERMS.DCMIType	text
DCTERMS.issued' scheme='DCTERMS.W3CDTF	2000-11-15
DCTERMS.abstract	形式的手法の設計導入教育への適用の有用性を調べるために，大阪大学基礎工学部情報科学科3年次学生のCPU設計実験において，(i)我々の研究グループで作成した検証システムを用いて設計の正しさを形式的に証明する設計手法（新手法），(ii)慎重な見直しや波形シミュレーションなどで設計の正しさを確認する設計手法（従来手法），の2つのコースを設けて，その2つのコース間で作業時間と設計したCPUにおける誤りの有無について2カ年にわたって比較を行った．定められた中間レポート提出期限までに誤りのないCPUを設計した学生は，従来手法コースでは42人中0人，新手法コースでは42人中41人であった．従来手法コースでは提出期限後に，教官が誤りを指摘して学生が設計を修正する期間を設け，この期間に19人が誤りのないCPUを設計した．中間レポート提出期限までに費やした全作業時間の平均は新手法43時間に比べて従来手法のほうが13時間ほど短かった．以上より，あらかじめ定められた期限までに正しいCPUを設計するためには，新手法は30%ほど作業時間がかかるものの効果的であることが確かめられた.
DCTERMS.abstract	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.
DC.rights	ここに掲載した著作物の利用に関する注意本著作物の著作権は情報処理学会に帰属します。本著作物は著作権者である情報処理学会の許可のもとに掲載するものです。ご利用に当たっては「著作権法」ならびに「情報処理学会倫理綱領」に従うことをお願いいたします。
DC.rights	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.
DC.format	application/pdf
citation_title	CPU設計導入教育への形式的設計検証手法の適用
	Applying Formal Verification Method to Education in Design of CPU
	CPU　セッケイ　ドウニュウ　キョウイク　ヘノ　ケイシキテキ　セッケイ　ケンショウ　シュホウ　ノ　テキヨウ
citation_author	北浜, 優子
	キタハマ, ユウコ
	Kitahama, Yuko
	北嶋, 曉
	キタジマ, アキラ
	Kitajima, Akira
	岡野, 浩三
	オカノ, コウゾウ
	Okano, Kozo
	谷口, 健一
	タニグチ, ケンイチ
	Taniguchi, Kenichi
citation_publisher	情報処理学会
citation_publisher	ジョウホウ　ショリ　ガッカイ
citation_language	日本語
citation_date	2000-11-15
citation_journal_title	情報処理学会論文誌
citation_volume	41
citation_issue	11
citation_firstpage	3114
citation_lastpage	3121
citation_public_url	https://hdl.handle.net/11094/50250

閲覧可能ファイル

論文情報

論文詳細を表示