Chulalongkorn University Theses and Dissertations (Chula ETD)
การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์
Other Title (Parallel Title in Other Language of ETD)
Formal verification at a register transfer level of a processor by symbolic model checking
Year (A.D.)
2002
Document Type
Thesis
First Advisor
ประภาส จงสถิตย์วัฒนา
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Degree Name
วิศวกรรมศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิศวกรรมคอมพิวเตอร์
DOI
10.58837/CHULA.THE.2002.1446
Abstract
นำเสนอการทวนสอบรูปนัยของหน่วยประมวลผล ที่ถูกออกแบบเพื่อใช้ในระบบเว็บเซิร์ฟเวอร์แบบฝังตัว โดยที่การทวนสอบกระทำกับรายละเอียดการออกแบบในระดับถ่ายโอนเรจิสเตอร์ ซึ่งเป็นระดับที่สามารถนำไปสังเคราะห์วงจรได้ ในการทวนสอบจะทำโดยใช้โปรแกรมคาเดนค์เอสเอมวี ซึ่งทำงานโดยใช้เทคนิคการตรวจสอบแบบจำลองเชิงสัญลักษณ์ ซึ่งมีปัญหาการเพิ่มอย่างรวดเร็วของสถานะ ในวิทยานิพนธ์จึงนำเสนอวิธีต่างๆ ที่ใช้แก้ปัญหาดังกล่าว และในวิทยานิพนธ์นี้ยังได้นำเสนอวิธีทวนสอบแบบลำดับขั้น ซึ่งแบ่งการทวนสอบเป็นหลายขั้นตอน โดยแต่ละขั้นตอนจะมีรายละเอียดเพิ่มขึ้นจากขั้นตอนแรกไปจนถึงขั้นตอนสุดท้าย ซึ่งวิธีการนี้ช่วยทำให้การหาสาเหตุของปัญหาทำได้ง่ายขึ้น ในกรณีที่เกิดข้อผิดพลาดในวงจรและทำให้สามารถทวนสอบได้เสร็จในเวลาที่สมเหตุผล การทวนสอบได้กระทำกับหน่วยประมวลผลที่ไม่ซับซ้อน และกระบวนการทวนสอบสามารถกระทำได้สำเร็จ
Other Abstract (Other language abstract of ETD)
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.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
บวรภราดร, ประพนธ์, "การทวนสอบรูปนัยในระดับถ่ายโอนเรจิสเตอร์ของหน่วยประมวลผล โดยการตรวจสอบแบบจำลองเชิงสัญลักษณ์" (2002). Chulalongkorn University Theses and Dissertations (Chula ETD). 64673.
https://digital.car.chula.ac.th/chulaetd/64673