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

Formal verification at a register transfer level of a processor by symbolic model checking

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

ThaSH: ระบบคอมพิวเตอร์ -- การทวนสอบ

ThaSH: คอมพิวเตอร์ -- การทดสอบ

Abstract: นำเสนอการทวนสอบรูปนัยของหน่วยประมวลผล ที่ถูกออกแบบเพื่อใช้ในระบบเว็บเซิร์ฟเวอร์แบบฝังตัว โดยที่การทวนสอบกระทำกับรายละเอียดการออกแบบในระดับถ่ายโอนเรจิสเตอร์ ซึ่งเป็นระดับที่สามารถนำไปสังเคราะห์วงจรได้ ในการทวนสอบจะทำโดยใช้โปรแกรมคาเดนค์เอสเอมวี ซึ่งทำงานโดยใช้เทคนิคการตรวจสอบแบบจำลองเชิงสัญลักษณ์ ซึ่งมีปัญหาการเพิ่มอย่างรวดเร็วของสถานะ ในวิทยานิพนธ์จึงนำเสนอวิธีต่างๆ ที่ใช้แก้ปัญหาดังกล่าว และในวิทยานิพนธ์นี้ยังได้นำเสนอวิธีทวนสอบแบบลำดับขั้น ซึ่งแบ่งการทวนสอบเป็นหลายขั้นตอน โดยแต่ละขั้นตอนจะมีรายละเอียดเพิ่มขึ้นจากขั้นตอนแรกไปจนถึงขั้นตอนสุดท้าย ซึ่งวิธีการนี้ช่วยทำให้การหาสาเหตุของปัญหาทำได้ง่ายขึ้น ในกรณีที่เกิดข้อผิดพลาดในวงจรและทำให้สามารถทวนสอบได้เสร็จในเวลาที่สมเหตุผล การทวนสอบได้กระทำกับหน่วยประมวลผลที่ไม่ซับซ้อน และกระบวนการทวนสอบสามารถกระทำได้สำเร็จ

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.

จุฬาลงกรณ์มหาวิทยาลัย. สำนักงานวิทยทรัพยากร

Address: กรุงเทพมหานคร

Email: cuir@car.chula.ac.th

Name: ประภาส จงสถิตย์วัฒนา

Role: ที่ปรึกษา

Created: 2545

Modified: 2560-05-16

Issued: 2560-03-26

วิทยานิพนธ์/Thesis

application/pdf

ISBN: 9741715374

tha

DegreeName: วิศวกรรมศาสตรมหาบัณฑิต

Level: ปริญญาโท

Descipline: วิศวกรรมคอมพิวเตอร์

Grantor: จุฬาลงกรณ์มหาวิทยาลัย

©copyrights จุฬาลงกรณ์มหาวิทยาลัย

ลำดับที่.	ชื่อแฟ้มข้อมูล	ขนาดแฟ้มข้อมูล	จำนวนเข้าถึง	วัน-เวลาเข้าถึงล่าสุด
1	Prapon[1].pdf	847.63 KB	2	2023-12-27 10:50:07

ใช้เวลา

0.020228 วินาที