Terminal Satisfiability in GSTE
المؤلفون المشاركون
Chang, Zhengwei
Zheng, Desheng
Guo, Wensheng
Xu, Yongsheng
Yang, Guowu
المصدر
Journal of Applied Mathematics
العدد
المجلد 2014، العدد 2014 (31 ديسمبر/كانون الأول 2014)، ص ص. 1-10، 10ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2014-05-15
دولة النشر
مصر
عدد الصفحات
10
التخصصات الرئيسية
الملخص EN
Generalized symbolic trajectory evaluation (GSTE) is an extension of symbolic trajectory evaluation (STE) and a method of model checking.
GSTE specifications are given as assertion graphs.
There are four efficient methods to verify whether a circuit model obeys an assertion graph in GSTE, Model Checking Strong Satisfiability (SMC), Model Checking Normal Satisfiability (NMC), Model Checking Fair Satisfiability (FMC), and Model Checking Terminal Satisfiability (TMC).
SMC, NMC, and FMC have been proved and applied in industry, but TMC has not.
This paper gives a six-tuple definition and presents a new algorithm for TMC.
Based on these, we prove that our algorithm is sound and complete.
It solves the SMC’s limitation (resulting in false negative) without extending from finite specification to infinite specification.
At last, a case of using TMC to verify a realistic hardware circuit round-robin arbiter is achieved.
Avoiding verifying the undesired paths which are not related to the specifications, TMC makes it possible to reduce the computational complexity, and the experimental results suggest that the time cost by SMC is 3.14× with TMC in the case.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Xu, Yongsheng& Yang, Guowu& Chang, Zhengwei& Zheng, Desheng& Guo, Wensheng. 2014. Terminal Satisfiability in GSTE. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-10.
https://search.emarefa.net/detail/BIM-493632
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Xu, Yongsheng…[et al.]. Terminal Satisfiability in GSTE. Journal of Applied Mathematics No. 2014 (2014), pp.1-10.
https://search.emarefa.net/detail/BIM-493632
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Xu, Yongsheng& Yang, Guowu& Chang, Zhengwei& Zheng, Desheng& Guo, Wensheng. Terminal Satisfiability in GSTE. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-10.
https://search.emarefa.net/detail/BIM-493632
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-493632
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر