Terminal Satisfiability in GSTEReportar como inadecuado

Terminal Satisfiability in GSTE - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Journal of Applied Mathematics - Volume 2014 2014, Article ID 725275, 10 pages -

Research Article

School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, Sichuan 611731, China

State Grid Sichuan Electric Power Research Institute, Chengdu, Sichuan 610000, China

Received 9 February 2014; Accepted 10 March 2014; Published 15 May 2014

Academic Editor: Guiming Luo

Copyright © 2014 Yongsheng Xu et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.


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.

Autor: Yongsheng Xu, Guowu Yang, Zhengwei Chang, Desheng Zheng, and Wensheng Guo

Fuente: https://www.hindawi.com/


Documentos relacionados