Terminal Satisfiability in GSTE

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

Journal of Applied Mathematics, 2014, vol. 2014, 1-10

Abstract:

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.

Date: 2014
References: Add references at CitEc
Citations:

Downloads: (external link)
http://downloads.hindawi.com/journals/JAM/2014/725275.pdf (application/pdf)
http://downloads.hindawi.com/journals/JAM/2014/725275.xml (text/xml)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:hin:jnljam:725275

DOI: 10.1155/2014/725275

Access Statistics for this article

More articles in Journal of Applied Mathematics from Hindawi
Bibliographic data for series maintained by Mohamed Abdelhakeem ().