การสร้างแบบจำลองด้วยโพรเมลาเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในการสร้างวงจรอสมวาร

คณุตม์ บุญเรืองขาว

Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/59619

Full metadata record

DC Field	Value	Language
dc.contributor.advisor	อาทิตย์ ทองทักษ์	-
dc.contributor.advisor	วิวัฒน์ วัฒนาวุฒิ	-
dc.contributor.author	คณุตม์ บุญเรืองขาว	-
dc.contributor.other	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์	-
dc.date.accessioned	2018-09-14T05:09:57Z	-
dc.date.available	2018-09-14T05:09:57Z	-
dc.date.issued	2560	-
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/59619	-
dc.description	วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2560	-
dc.description.abstract	การทวนสอบวงจรอสมวารนั้นมีความจำเป็นอย่างยิ่งในขั้นตอนการออกแบบเพื่อความถูกต้องในการทำงานของสัญญาณ โดยวงจรจะถูกออกแบบในขั้นต้นด้วยซิกแนลแทรนซิชันกราฟ วิทยานิพนธ์ใช้ประโยชน์จากเทคนิคการตรวจสอบแบบจำลองเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในคุณสมบัติซึ่งประกอบด้วย คุณสมบัติความปลอดภัย คุณสมบัติไลฟ์เนส คุณสมบัติความทนทาน คุณสมบัติความต้องกัน และคุณสมบัติการกำหนดสถานะสมบูรณ์ ซึ่งซิกแนลแทนซิชันกราฟประกอบด้วยประเภทวัฏจักรเชิงเดี่ยว และประเภทวัฏจักรหลากหลาย ในขั้นแรกซิกแนลแทรนซิชันกราฟจะถูกแปลงเป็นรหัสโพรเมลาแบบจำลองโครงสร้าง และแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน จากนั้นจึงนำซิกแนลแทรนซิชันกราฟไปแปลงเป็นตรรกะเวลาเชิงเส้นซึ่งประกอบด้วยคุณสมบัติความปลอดภัย คุณสมบัติไลฟ์เนส คุณสมบัติความทนทาน คุณสมบัติความต้องกัน และคุณสมบัติการกำหนดสถานะที่สมบูรณ์ จากนั้นคุณสมบัติความปลอดภัยจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติความปลอดภัยไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติไลฟ์เนสจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติไลฟ์เนสไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติความทนทานจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติความทนทานไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติความต้องกันจะทวนสอบโดยนำรหัสโพรเมลาแบบแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน และตรรกะเวลาเชิงเส้นของคุณสมบัติความต้องกันไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ ในขั้นสุดท้ายคุณสมบัติการกำหนดสถานะที่สมบูรณ์จะนำรหัสโพรเมลาแบบแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน และตรรกะเวลาเชิงเส้นของการกำหนดสถานะที่สมบูรณ์มาเพื่อหาความสัมพันธ์เชิงล็อคและทวนสอบโดยเครื่องมือสปิน จากนั้นจึงนำผลที่ได้จากการจำลองมาตรวจสอบในเครื่องมือที่พัฒนาขึ้นจึงได้คำตอบของการทวนสอบคุณสมบัตินี้ อย่างไรก็ตามเทคนิคของงานวิจัยนี้ยังไม่เป็นอัตโนมัติในบางคุณสมบัติ	-
dc.description.abstractalternative	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.	-
dc.language.iso	th	-
dc.publisher	จุฬาลงกรณ์มหาวิทยาลัย	-
dc.relation.uri	http://doi.org/10.58837/CHULA.THE.2017.1369	-
dc.rights	จุฬาลงกรณ์มหาวิทยาลัย	-
dc.subject	วงจรอะซิงโครนัส	-
dc.subject	Asynchronous circuits	-
dc.title	การสร้างแบบจำลองด้วยโพรเมลาเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในการสร้างวงจรอสมวาร	-
dc.title.alternative	A MODEL CONSTRUCTION BY PROMELA FOR SIGNAL TRANSITION GRAPH VERIFICATION IN ASYNCHRONOUS CIRCUIT IMPLEMENTATION	-
dc.type	Thesis	-
dc.degree.name	วิศวกรรมศาสตรมหาบัณฑิต	-
dc.degree.level	ปริญญาโท	-
dc.degree.discipline	วิศวกรรมคอมพิวเตอร์	-
dc.degree.grantor	จุฬาลงกรณ์มหาวิทยาลัย	-
dc.email.advisor	Arthit.T@Chula.ac.th,arthit.t@chula.ac.th	-
dc.email.advisor	Wiwat.V@Chula.ac.th,wiwatv@gmail.com	-
dc.identifier.DOI	10.58837/CHULA.THE.2017.1369	-
Appears in Collections:	Eng - Theses

Files in This Item:

File	Description	Size	Format
5870390321.pdf		10.01 MB	Adobe PDF	View/Open

Show simple item record