Journal of Applied Mathematics
Volume 2013 (2013), Article ID 709071, 7 pages
http://dx.doi.org/10.1155/2013/709071
Research Article

A Transformation-Based Approach to Implication of GSTE Assertion Graphs

1School of Computer Science and Engineering, University of Electronic Science and Technology Chengdu, Sichuan 610054, China
2Synopsys Inc., Mountain View, CA 94043, USA
3Department of ECE, Portland State University, Portland, Oregon, USA

Received 8 February 2013; Accepted 13 May 2013

Academic Editor: Guiming Luo

Copyright © 2013 Guowu Yang 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.

Abstract

Generalized symbolic trajectory evaluation (GSTE) is a model checking approach and has successfully demonstrated its powerful capacity in formal verification of VLSI systems. GSTE is an extension of symbolic trajectory evaluation (STE) to the model checking of -regular properties. It is an alternative to classical model checking algorithms where properties are specified as finite-state automata. In GSTE, properties are specified as assertion graphs, which are labeled directed graphs where each edge is labeled with two labeling functions: antecedent and consequent. In this paper, we show the complement relation between GSTE assertion graphs and finite-state automata with the expressiveness of regular languages and -regular languages. We present an algorithm that transforms a GSTE assertion graph to a finite-state automaton and vice versa. By applying this algorithm, we transform the problem of GSTE assertion graphs implication to the problem of automata language containment. We demonstrate our approach with its application to verification of an FIFO circuit.