การทวนสอบวงจรสามารถเลือกทำได้โดยการตรวจสอบพฤติกรรมของวงจรที่เขียนขึ้นด้วยซิกแนลทรานสิชันกราฟหรือที่เรียกว่าเอสทีจีกับวงจรที่ได้จากการสังเคราะห์ วิทยานิพนธ์ฉบับนี้ใช้ประโยชน์จากเทคนิคการจำลองลำดับสัญญาณเพื่อทวนสอบวงจรอสมวารแบบวัฏจักรเชิงเดียวและวัฏจักรที่มีจุดยอดไม่ซ้ำกันเท่านั้น ประการแรกพฤติกรรมของวงจรที่ต้องการเขียนในรูปแบบของเอสทีจีและวงจรที่ได้จากการสังเคราะห์นั้นจะถูกแปลงให้เป็นภาษาโพรเมล่า จากนั้นสปินจะถูกใช้เป็นเครื่องมือในการจำลองการทำงานรหัสภาษาโพรเมล่าที่แปลงมาได้นั้น และเอาต์พุตที่ได้จากการจำลองจะถูกบันทึกเป็นลำดับการเปลี่ยนแปลงสัญญาณจากการจำลองการทำงานของวงจรเป้าหมายหรือที่เรียกว่าเอสเอส ประการที่สองผู้วิจัยจะค้นหารูปแบบพฤติกรรมที่สำคัญของวงจรที่เรียกว่าลำดับการเปลี่ยนแปลงสัญญาณที่เป็นไปได้ทั้งหมดหรือเรียกสั้นๆ ว่าเอสทีเอส และลำดับความสัมพันธ์เชิงล็อค หรือเรียกสั้นๆ ว่า แอลอาร์เอสจากเอสทีจีที่กำหนด ประการที่สามคุณสมบัติไลฟ์เนสและคุณสมบัติความทนทานจะถูกทวนสอบด้วยวิธีการค้นหารูปแบบพฤติกรรมเอสทีเอสและแอลอาร์เอสออกจากเอสเอส เครื่องมือที่ใช้ในการค้นหาถูกพัฒนาขึ้นเพื่อสนับสนุนการค้นหารูปแบบพฤติกรรมดังกล่าว การออกแบบของวงจรส่วนย่อยซีจะถูกใช้เป็นกรณีศึกษาของงานวิจัยนี้ เราสามารถรายงานผลลัพธ์ความสำเร็จจากการทวนสอบภายในเวลาที่ยอมรับได้ อย่างไรก็ตามข้อจำกัดของเทคนิคการจำลองลำดับสัญญาณนี้ยังไม่เป็นนิยมในการออกแบบวงจรที่มีขนาดใหญ่และมีความซับซ้อน

วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2557