การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์
วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2545
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Theses and Dissertations |
| Language: | Thai |
| Published: |
จุฬาลงกรณ์มหาวิทยาลัย
2009
|
| Subjects: | |
| Online Access: | http://cuir.car.chula.ac.th/handle/123456789/10544 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Chulalongkorn University |
| Language: | Thai |
| id |
th-cuir.10544 |
|---|---|
| record_format |
dspace |
| spelling |
th-cuir.105442009-08-26T09:14:21Z การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์ Formal verification at a register transfer level of a processor by symbolic model checking ประพนธ์ บวรภราดร ประภาส จงสถิตย์วัฒนา จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ ระบบคอมพิวเตอร์ -- การทวนสอบ คอมพิวเตอร์ -- การทดสอบ วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2545 นำเสนอการทวนสอบรูปนัยของหน่วยประมวลผล ที่ถูกออกแบบเพื่อใช้ในระบบเว็บเซิร์ฟเวอร์แบบฝังตัว โดยที่การทวนสอบกระทำกับรายละเอียดการออกแบบในระดับถ่ายโอนเรจิสเตอร์ ซึ่งเป็นระดับที่สามารถนำไปสังเคราะห์วงจรได้ ในการทวนสอบจะทำโดยใช้โปรแกรมคาเดนค์เอสเอมวี ซึ่งทำงานโดยใช้เทคนิคการตรวจสอบแบบจำลองเชิงสัญลักษณ์ ซึ่งมีปัญหาการเพิ่มอย่างรวดเร็วของสถานะ ในวิทยานิพนธ์จึงนำเสนอวิธีต่างๆ ที่ใช้แก้ปัญหาดังกล่าว และในวิทยานิพนธ์นี้ยังได้นำเสนอวิธีทวนสอบแบบลำดับขั้น ซึ่งแบ่งการทวนสอบเป็นหลายขั้นตอน โดยแต่ละขั้นตอนจะมีรายละเอียดเพิ่มขึ้นจากขั้นตอนแรกไปจนถึงขั้นตอนสุดท้าย ซึ่งวิธีการนี้ช่วยทำให้การหาสาเหตุของปัญหาทำได้ง่ายขึ้น ในกรณีที่เกิดข้อผิดพลาดในวงจรและทำให้สามารถทวนสอบได้เสร็จในเวลาที่สมเหตุผล การทวนสอบได้กระทำกับหน่วยประมวลผลที่ไม่ซับซ้อน และกระบวนการทวนสอบสามารถกระทำได้สำเร็จ 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. 2009-08-26T09:14:20Z 2009-08-26T09:14:20Z 2545 Thesis 9741715374 http://cuir.car.chula.ac.th/handle/123456789/10544 th จุฬาลงกรณ์มหาวิทยาลัย 867971 bytes application/pdf application/pdf จุฬาลงกรณ์มหาวิทยาลัย |
| institution |
Chulalongkorn University |
| building |
Chulalongkorn University Library |
| country |
Thailand |
| collection |
Chulalongkorn University Intellectual Repository |
| language |
Thai |
| topic |
ระบบคอมพิวเตอร์ -- การทวนสอบ คอมพิวเตอร์ -- การทดสอบ |
| spellingShingle |
ระบบคอมพิวเตอร์ -- การทวนสอบ คอมพิวเตอร์ -- การทดสอบ ประพนธ์ บวรภราดร การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์ |
| description |
วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2545 |
| author2 |
ประภาส จงสถิตย์วัฒนา |
| author_facet |
ประภาส จงสถิตย์วัฒนา ประพนธ์ บวรภราดร |
| format |
Theses and Dissertations |
| author |
ประพนธ์ บวรภราดร |
| author_sort |
ประพนธ์ บวรภราดร |
| title |
การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์ |
| title_short |
การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์ |
| title_full |
การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์ |
| title_fullStr |
การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์ |
| title_full_unstemmed |
การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์ |
| title_sort |
การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์ |
| publisher |
จุฬาลงกรณ์มหาวิทยาลัย |
| publishDate |
2009 |
| url |
http://cuir.car.chula.ac.th/handle/123456789/10544 |
| _version_ |
1681414037907177472 |