Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/10544
| Title: | การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์ |
| Other Titles: | Formal verification at a register transfer level of a processor by symbolic model checking |
| Authors: | ประพนธ์ บวรภราดร |
| Advisors: | ประภาส จงสถิตย์วัฒนา |
| Other author: | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ |
| Advisor's Email: | Prabhas.C@chula.ac.th |
| Subjects: | ระบบคอมพิวเตอร์ -- การทวนสอบ คอมพิวเตอร์ -- การทดสอบ |
| Issue Date: | 2545 |
| Publisher: | จุฬาลงกรณ์มหาวิทยาลัย |
| Abstract: | นำเสนอการทวนสอบรูปนัยของหน่วยประมวลผล ที่ถูกออกแบบเพื่อใช้ในระบบเว็บเซิร์ฟเวอร์แบบฝังตัว โดยที่การทวนสอบกระทำกับรายละเอียดการออกแบบในระดับถ่ายโอนเรจิสเตอร์ ซึ่งเป็นระดับที่สามารถนำไปสังเคราะห์วงจรได้ ในการทวนสอบจะทำโดยใช้โปรแกรมคาเดนค์เอสเอมวี ซึ่งทำงานโดยใช้เทคนิคการตรวจสอบแบบจำลองเชิงสัญลักษณ์ ซึ่งมีปัญหาการเพิ่มอย่างรวดเร็วของสถานะ ในวิทยานิพนธ์จึงนำเสนอวิธีต่างๆ ที่ใช้แก้ปัญหาดังกล่าว และในวิทยานิพนธ์นี้ยังได้นำเสนอวิธีทวนสอบแบบลำดับขั้น ซึ่งแบ่งการทวนสอบเป็นหลายขั้นตอน โดยแต่ละขั้นตอนจะมีรายละเอียดเพิ่มขึ้นจากขั้นตอนแรกไปจนถึงขั้นตอนสุดท้าย ซึ่งวิธีการนี้ช่วยทำให้การหาสาเหตุของปัญหาทำได้ง่ายขึ้น ในกรณีที่เกิดข้อผิดพลาดในวงจรและทำให้สามารถทวนสอบได้เสร็จในเวลาที่สมเหตุผล การทวนสอบได้กระทำกับหน่วยประมวลผลที่ไม่ซับซ้อน และกระบวนการทวนสอบสามารถกระทำได้สำเร็จ |
| Other Abstract: | 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. |
| Description: | วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2545 |
| Degree Name: | วิศวกรรมศาสตรมหาบัณฑิต |
| Degree Level: | ปริญญาโท |
| Degree Discipline: | วิศวกรรมคอมพิวเตอร์ |
| URI: | http://cuir.car.chula.ac.th/handle/123456789/10544 |
| ISBN: | 9741715374 |
| Type: | Thesis |
| Appears in Collections: | Eng - Theses |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| Prapon.pdf | 847.63 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.