|
การสร้างแบบจำลองด้วยโพรเมลาเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในการสร้างวงจรอสมวาร |
|---|---|
| รหัสดีโอไอ | |
| Title | การสร้างแบบจำลองด้วยโพรเมลาเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในการสร้างวงจรอสมวาร |
| Creator | คณุตม์ บุญเรืองขาว |
| Contributor | อาทิตย์ ทองทักษ์, วิวัฒน์ วัฒนาวุฒิ |
| Publisher | จุฬาลงกรณ์มหาวิทยาลัย |
| Publication Year | 2560 |
| Keyword | วงจรอะซิงโครนัส, Asynchronous circuits |
| Abstract | การทวนสอบวงจรอสมวารนั้นมีความจำเป็นอย่างยิ่งในขั้นตอนการออกแบบเพื่อความถูกต้องในการทำงานของสัญญาณ โดยวงจรจะถูกออกแบบในขั้นต้นด้วยซิกแนลแทรนซิชันกราฟ วิทยานิพนธ์ใช้ประโยชน์จากเทคนิคการตรวจสอบแบบจำลองเพื่อทวนสอบซิกแนลแทรนซิชันกราฟในคุณสมบัติซึ่งประกอบด้วย คุณสมบัติความปลอดภัย คุณสมบัติไลฟ์เนส คุณสมบัติความทนทาน คุณสมบัติความต้องกัน และคุณสมบัติการกำหนดสถานะสมบูรณ์ ซึ่งซิกแนลแทนซิชันกราฟประกอบด้วยประเภทวัฏจักรเชิงเดี่ยว และประเภทวัฏจักรหลากหลาย ในขั้นแรกซิกแนลแทรนซิชันกราฟจะถูกแปลงเป็นรหัสโพรเมลาแบบจำลองโครงสร้าง และแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน จากนั้นจึงนำซิกแนลแทรนซิชันกราฟไปแปลงเป็นตรรกะเวลาเชิงเส้นซึ่งประกอบด้วยคุณสมบัติความปลอดภัย คุณสมบัติไลฟ์เนส คุณสมบัติความทนทาน คุณสมบัติความต้องกัน และคุณสมบัติการกำหนดสถานะที่สมบูรณ์ จากนั้นคุณสมบัติความปลอดภัยจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติความปลอดภัยไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติไลฟ์เนสจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติไลฟ์เนสไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติความทนทานจะทวนสอบโดยนำรหัสโพรเมลาแบบจำลองโครงสร้าง และตรรกะเวลาเชิงเส้นของคุณสมบัติความทนทานไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ คุณสมบัติความต้องกันจะทวนสอบโดยนำรหัสโพรเมลาแบบแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน และตรรกะเวลาเชิงเส้นของคุณสมบัติความต้องกันไปทวนสอบโดยเครื่องมือสปินจะได้ผลการทวนสอบของคุณสมบัติ ในขั้นสุดท้ายคุณสมบัติการกำหนดสถานะที่สมบูรณ์จะนำรหัสโพรเมลาแบบแบบจำลองวัฏจักรที่มีจุดยอดไม่ซ้ำกัน และตรรกะเวลาเชิงเส้นของการกำหนดสถานะที่สมบูรณ์มาเพื่อหาความสัมพันธ์เชิงล็อคและทวนสอบโดยเครื่องมือสปิน จากนั้นจึงนำผลที่ได้จากการจำลองมาตรวจสอบในเครื่องมือที่พัฒนาขึ้นจึงได้คำตอบของการทวนสอบคุณสมบัตินี้ อย่างไรก็ตามเทคนิคของงานวิจัยนี้ยังไม่เป็นอัตโนมัติในบางคุณสมบัติ |
| URL Website | cuir.car.chula.ac.th |
