Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/45948
| Title: | การทวนสอบวงจรอสมวารด้วยการจำลองลำดับสัญญาณในเอสทีจี |
| Other Titles: | ASYNCHRONOUS CIRCUIT VERIFICATION USING SIGNAL SEQUENCE SIMLULATION IN STG |
| Authors: | วีระศักดิ์ ล่อซุ่นนี้ |
| Advisors: | วิวัฒน์ วัฒนาวุฒิ อาทิตย์ ทองทักษ์ |
| Other author: | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ |
| Advisor's Email: | Wiwat.V@Chula.ac.th,wiwatv@gmail.com,wiwat@chula.ac.th Arthit.T@Chula.ac.th |
| Issue Date: | 2557 |
| Publisher: | จุฬาลงกรณ์มหาวิทยาลัย |
| Abstract: | การทวนสอบวงจรสามารถเลือกทำได้โดยการตรวจสอบพฤติกรรมของวงจรที่เขียนขึ้นด้วยซิกแนลทรานสิชันกราฟหรือที่เรียกว่าเอสทีจีกับวงจรที่ได้จากการสังเคราะห์ วิทยานิพนธ์ฉบับนี้ใช้ประโยชน์จากเทคนิคการจำลองลำดับสัญญาณเพื่อทวนสอบวงจรอสมวารแบบวัฏจักรเชิงเดียวและวัฏจักรที่มีจุดยอดไม่ซ้ำกันเท่านั้น ประการแรกพฤติกรรมของวงจรที่ต้องการเขียนในรูปแบบของเอสทีจีและวงจรที่ได้จากการสังเคราะห์นั้นจะถูกแปลงให้เป็นภาษาโพรเมล่า จากนั้นสปินจะถูกใช้เป็นเครื่องมือในการจำลองการทำงานรหัสภาษาโพรเมล่าที่แปลงมาได้นั้น และเอาต์พุตที่ได้จากการจำลองจะถูกบันทึกเป็นลำดับการเปลี่ยนแปลงสัญญาณจากการจำลองการทำงานของวงจรเป้าหมายหรือที่เรียกว่าเอสเอส ประการที่สองผู้วิจัยจะค้นหารูปแบบพฤติกรรมที่สำคัญของวงจรที่เรียกว่าลำดับการเปลี่ยนแปลงสัญญาณที่เป็นไปได้ทั้งหมดหรือเรียกสั้นๆ ว่าเอสทีเอส และลำดับความสัมพันธ์เชิงล็อค หรือเรียกสั้นๆ ว่า แอลอาร์เอสจากเอสทีจีที่กำหนด ประการที่สามคุณสมบัติไลฟ์เนสและคุณสมบัติความทนทานจะถูกทวนสอบด้วยวิธีการค้นหารูปแบบพฤติกรรมเอสทีเอสและแอลอาร์เอสออกจากเอสเอส เครื่องมือที่ใช้ในการค้นหาถูกพัฒนาขึ้นเพื่อสนับสนุนการค้นหารูปแบบพฤติกรรมดังกล่าว การออกแบบของวงจรส่วนย่อยซีจะถูกใช้เป็นกรณีศึกษาของงานวิจัยนี้ เราสามารถรายงานผลลัพธ์ความสำเร็จจากการทวนสอบภายในเวลาที่ยอมรับได้ อย่างไรก็ตามข้อจำกัดของเทคนิคการจำลองลำดับสัญญาณนี้ยังไม่เป็นนิยมในการออกแบบวงจรที่มีขนาดใหญ่และมีความซับซ้อน |
| Other Abstract: | The circuit verification can be alternatively conducted by verifying a circuit behavior, drawn using Signal Transition Graph or called STG, against the circuit implementation. This thesis exploits the Signal Sequence Simulation Technique to the verification of an asynchronous circuit with single and simple cycle only. Firstly, the expected circuit behavior, in STG, and its implementation are converted in Promela codes. The SPIN is used to simulate these Promela codes and the output of the simulation would be recorded as the Signal Sequence, called SS, of the target circuit. Secondly, we extract two important expected behavioral patterns of the circuit called the Signal Transition Sequence, or STS in short, and the Lock Relation Sequence, or LRS in short, from the given STG. Thirdly, both Liveness and Persistence properties are verified according to the searching STS and LRS behavioral patterns out of the given SS. The searching tools are developed to support the mentioned searching of the behavioral patterns. The C-element circuit designs are used as our case studies. The verification results are successfully reported with the acceptable simulation time. However, the limitation of this signal sequence simulation technique is still not preferable to the huge and complex asynchronous circuit design. |
| Description: | วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2557 |
| Degree Name: | วิทยาศาสตรมหาบัณฑิต |
| Degree Level: | ปริญญาโท |
| Degree Discipline: | วิศวกรรมซอฟต์แวร์ |
| URI: | http://cuir.car.chula.ac.th/handle/123456789/45948 |
| Type: | Thesis |
| Appears in Collections: | Eng - Theses |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 5471008521.pdf | 3.96 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.