Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
A MODEL CONSTRUCTION BY PROMELA FOR SIGNAL TRANSITION GRAPH VERIFICATION IN ASYNCHRONOUS CIRCUIT IMPLEMENTATION
Year (A.D.)
2017
Document Type
Thesis
First Advisor
อาทิตย์ ทองทักษ์
Second Advisor
วิวัฒน์ วัฒนาวุฒิ
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Department (if any)
Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)
Degree Name
วิศวกรรมศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิศวกรรมคอมพิวเตอร์
DOI
10.58837/CHULA.THE.2017.1369
Abstract
การทวนสอบวงจรอสมวารนั้นมีความจำเป็นอย่างยิ่งในขั้นตอนการออกแบบเพื่อความถูกต้องในการทำงานของสัญญาณ โดยวงจรจะถูกออกแบบในขั้นต้นด้วยซิกแนลแทรนซิชันกราฟ วิทยานิพนธ์ใช้ประโยชน์จากเทคนิคการตรวจสอบแบบจำลองเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในคุณสมบัติซึ่งประกอบด้วย คุณสมบัติความปลอดภัย คุณสมบัติไลฟ์เนส คุณสมบัติความทนทาน คุณสมบัติความต้องกัน และคุณสมบัติการกำหนดสถานะสมบูรณ์ ซึ่งซิกแนลแทนซิชันกราฟประกอบด้วยประเภทวัฏจักรเชิงเดี่ยว และประเภทวัฏจักรหลากหลาย ในขั้นแรกซิกแนลแทรนซิชันกราฟจะถูกแปลงเป็นรหัสโพรเมลาแบบจำลองโครงสร้าง และแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน จากนั้นจึงนำซิกแนลแทรนซิชันกราฟไปแปลงเป็นตรรกะเวลาเชิงเส้นซึ่งประกอบด้วยคุณสมบัติความปลอดภัย คุณสมบัติไลฟ์เนส คุณสมบัติความทนทาน คุณสมบัติความต้องกัน และคุณสมบัติการกำหนดสถานะที่สมบูรณ์ จากนั้นคุณสมบัติความปลอดภัยจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติความปลอดภัยไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติไลฟ์เนสจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติไลฟ์เนสไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติความทนทานจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติความทนทานไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติความต้องกันจะทวนสอบโดยนำรหัสโพรเมลาแบบแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน และตรรกะเวลาเชิงเส้นของคุณสมบัติความต้องกันไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ ในขั้นสุดท้ายคุณสมบัติการกำหนดสถานะที่สมบูรณ์จะนำรหัสโพรเมลาแบบแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน และตรรกะเวลาเชิงเส้นของการกำหนดสถานะที่สมบูรณ์มาเพื่อหาความสัมพันธ์เชิงล็อคและทวนสอบโดยเครื่องมือสปิน จากนั้นจึงนำผลที่ได้จากการจำลองมาตรวจสอบในเครื่องมือที่พัฒนาขึ้นจึงได้คำตอบของการทวนสอบคุณสมบัตินี้ อย่างไรก็ตามเทคนิคของงานวิจัยนี้ยังไม่เป็นอัตโนมัติในบางคุณสมบัติ
Other Abstract (Other language abstract of ETD)
Verification of asynchronous circuit is necessary in design phase, for the correctness of the signal operation. At First, the circuit will be designed by signal transition graph. This thesis exploits the model checking technique to verify signal transition graph in properties are safety liveness persistency consistency and Complete state coding (CSC).The types of signal transition graph are single- cycle and multi-cycle. At First, Signal transition graph is converted to Promela code type model structure and model simple-cycle, then Signal transition graph is converted Linear temporal logic (LTL) that consist of Safety, liveness, persistency, consistency and CSC. Then, safety property will check by Promela type model structure and LTL of safety property, verified by SPIN, the result will be shown. Then, liveness property will check by Promela type model structure and LTL of liveness property, verified by SPIN, the result will be shown. Then, persistency property will check by Promela type model structure and LTL of persistency property, verified by SPIN, the result will be shown. Then, consistency property will check by Promela type model simple-cycle and LTL of consistency property, verified by SPIN, the result will be shown. At last, CSC property will check by Promela type model simple-cycle and LTL of CSC property for lock relation checking and verified by SPIN, Then , the simulation result from SPIN will be investigate in the developed tool. The result will answered by the tool. However, the limitation of this thesis technique is not automatic in some properties.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
บุญเรืองขาว, คณุตม์, "การสร้างแบบจำลองด้วยโพรเมลาเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในการสร้างวงจรอสมวาร" (2017). Chulalongkorn University Theses and Dissertations (Chula ETD). 1859.
https://digital.car.chula.ac.th/chulaetd/1859