Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/59619
| Title: | การสร้างแบบจำลองด้วยโพรเมลาเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในการสร้างวงจรอสมวาร |
| Other Titles: | A MODEL CONSTRUCTION BY PROMELA FOR SIGNAL TRANSITION GRAPH VERIFICATION IN ASYNCHRONOUS CIRCUIT IMPLEMENTATION |
| Authors: | คณุตม์ บุญเรืองขาว |
| Advisors: | อาทิตย์ ทองทักษ์ วิวัฒน์ วัฒนาวุฒิ |
| Other author: | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ |
| Advisor's Email: | Arthit.T@Chula.ac.th,arthit.t@chula.ac.th Wiwat.V@Chula.ac.th,wiwatv@gmail.com |
| Subjects: | วงจรอะซิงโครนัส Asynchronous circuits |
| Issue Date: | 2560 |
| Publisher: | จุฬาลงกรณ์มหาวิทยาลัย |
| Abstract: | การทวนสอบวงจรอสมวารนั้นมีความจำเป็นอย่างยิ่งในขั้นตอนการออกแบบเพื่อความถูกต้องในการทำงานของสัญญาณ โดยวงจรจะถูกออกแบบในขั้นต้นด้วยซิกแนลแทรนซิชันกราฟ วิทยานิพนธ์ใช้ประโยชน์จากเทคนิคการตรวจสอบแบบจำลองเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในคุณสมบัติซึ่งประกอบด้วย คุณสมบัติความปลอดภัย คุณสมบัติไลฟ์เนส คุณสมบัติความทนทาน คุณสมบัติความต้องกัน และคุณสมบัติการกำหนดสถานะสมบูรณ์ ซึ่งซิกแนลแทนซิชันกราฟประกอบด้วยประเภทวัฏจักรเชิงเดี่ยว และประเภทวัฏจักรหลากหลาย ในขั้นแรกซิกแนลแทรนซิชันกราฟจะถูกแปลงเป็นรหัสโพรเมลาแบบจำลองโครงสร้าง และแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน จากนั้นจึงนำซิกแนลแทรนซิชันกราฟไปแปลงเป็นตรรกะเวลาเชิงเส้นซึ่งประกอบด้วยคุณสมบัติความปลอดภัย คุณสมบัติไลฟ์เนส คุณสมบัติความทนทาน คุณสมบัติความต้องกัน และคุณสมบัติการกำหนดสถานะที่สมบูรณ์ จากนั้นคุณสมบัติความปลอดภัยจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติความปลอดภัยไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติไลฟ์เนสจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติไลฟ์เนสไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติความทนทานจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติความทนทานไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติความต้องกันจะทวนสอบโดยนำรหัสโพรเมลาแบบแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน และตรรกะเวลาเชิงเส้นของคุณสมบัติความต้องกันไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ ในขั้นสุดท้ายคุณสมบัติการกำหนดสถานะที่สมบูรณ์จะนำรหัสโพรเมลาแบบแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน และตรรกะเวลาเชิงเส้นของการกำหนดสถานะที่สมบูรณ์มาเพื่อหาความสัมพันธ์เชิงล็อคและทวนสอบโดยเครื่องมือสปิน จากนั้นจึงนำผลที่ได้จากการจำลองมาตรวจสอบในเครื่องมือที่พัฒนาขึ้นจึงได้คำตอบของการทวนสอบคุณสมบัตินี้ อย่างไรก็ตามเทคนิคของงานวิจัยนี้ยังไม่เป็นอัตโนมัติในบางคุณสมบัติ |
| Other Abstract: | 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. |
| Description: | วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2560 |
| Degree Name: | วิศวกรรมศาสตรมหาบัณฑิต |
| Degree Level: | ปริญญาโท |
| Degree Discipline: | วิศวกรรมคอมพิวเตอร์ |
| URI: | http://cuir.car.chula.ac.th/handle/123456789/59619 |
| URI: | http://doi.org/10.58837/CHULA.THE.2017.1369 |
| metadata.dc.identifier.DOI: | 10.58837/CHULA.THE.2017.1369 |
| Type: | Thesis |
| Appears in Collections: | Eng - Theses |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 5870390321.pdf | 10.01 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.