การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์

ประพนธ์ บวรภราดร

Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/10544

Full metadata record

DC Field	Value	Language
dc.contributor.advisor	ประภาส จงสถิตย์วัฒนา	-
dc.contributor.author	ประพนธ์ บวรภราดร	-
dc.contributor.other	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์	-
dc.date.accessioned	2009-08-26T09:14:20Z	-
dc.date.available	2009-08-26T09:14:20Z	-
dc.date.issued	2545	-
dc.identifier.isbn	9741715374	-
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/10544	-
dc.description	วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2545	en
dc.description.abstract	นำเสนอการทวนสอบรูปนัยของหน่วยประมวลผล ที่ถูกออกแบบเพื่อใช้ในระบบเว็บเซิร์ฟเวอร์แบบฝังตัว โดยที่การทวนสอบกระทำกับรายละเอียดการออกแบบในระดับถ่ายโอนเรจิสเตอร์ ซึ่งเป็นระดับที่สามารถนำไปสังเคราะห์วงจรได้ ในการทวนสอบจะทำโดยใช้โปรแกรมคาเดนค์เอสเอมวี ซึ่งทำงานโดยใช้เทคนิคการตรวจสอบแบบจำลองเชิงสัญลักษณ์ ซึ่งมีปัญหาการเพิ่มอย่างรวดเร็วของสถานะ ในวิทยานิพนธ์จึงนำเสนอวิธีต่างๆ ที่ใช้แก้ปัญหาดังกล่าว และในวิทยานิพนธ์นี้ยังได้นำเสนอวิธีทวนสอบแบบลำดับขั้น ซึ่งแบ่งการทวนสอบเป็นหลายขั้นตอน โดยแต่ละขั้นตอนจะมีรายละเอียดเพิ่มขึ้นจากขั้นตอนแรกไปจนถึงขั้นตอนสุดท้าย ซึ่งวิธีการนี้ช่วยทำให้การหาสาเหตุของปัญหาทำได้ง่ายขึ้น ในกรณีที่เกิดข้อผิดพลาดในวงจรและทำให้สามารถทวนสอบได้เสร็จในเวลาที่สมเหตุผล การทวนสอบได้กระทำกับหน่วยประมวลผลที่ไม่ซับซ้อน และกระบวนการทวนสอบสามารถกระทำได้สำเร็จ	en
dc.description.abstractalternative	To propose a technique for formal verification of a processor used in an embedded web server. The verification process is performed at the RTL level of implementation, which can be synthesized by a synthesis tool. We use Cadence SMV tool, which employs the symbolic model checking technique, as the verification tool. This technique has the state explosion problem. In this thesis, we propose many methods to solve this problem. Furthermore, we propose a stepwise verification method that the details of design are increased in each step. This method makes the error finding process easier and enables the verification process to finish in a reasonable amount of time. The methods are illustrated on a simple processor. The whole design can be verified successfully.	en
dc.format.extent	867971 bytes	-
dc.format.mimetype	application/pdf	-
dc.language.iso	th	es
dc.publisher	จุฬาลงกรณ์มหาวิทยาลัย	en
dc.rights	จุฬาลงกรณ์มหาวิทยาลัย	en
dc.subject	ระบบคอมพิวเตอร์ -- การทวนสอบ	en
dc.subject	คอมพิวเตอร์ -- การทดสอบ	en
dc.title	การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์	en
dc.title.alternative	Formal verification at a register transfer level of a processor by symbolic model checking	en
dc.type	Thesis	es
dc.degree.name	วิศวกรรมศาสตรมหาบัณฑิต	es
dc.degree.level	ปริญญาโท	es
dc.degree.discipline	วิศวกรรมคอมพิวเตอร์	es
dc.degree.grantor	จุฬาลงกรณ์มหาวิทยาลัย	en
dc.email.advisor	Prabhas.C@chula.ac.th	-
Appears in Collections:	Eng - Theses

Files in This Item:

File	Description	Size	Format
Prapon.pdf		847.63 kB	Adobe PDF	View/Open

Show simple item record