A Transformation-Based Approach to Implication of GSTE Assertion Graphs

Authors

Gouwu Yang, University of Electronic Science and Technology Chengdu, Sichuan, ChinaFollow
William N. N. Hung, Synopsys Inc., Mountain View, CA
Xiaoyu Song, Portland State UniversityFollow
Wensheng Guo, University of Electronic Science and Technology Chengdu, Sichuan, China

Published In

Journal of Applied Mathematics

Document Type

Article

Publication Date

2013

Subjects

Assertion Graphs, Computer algorithims

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.

Description

Copyright (c) 2013 The Authors

This work is licensed under a Creative Commons Attribution 4.0 International License.

Locate the Document

https://doi-org/10.1155/2013/709071

DOI

10.1155/2013/709071

Persistent Identifier

https://archives.pdx.edu/ds/psu/33893

Citation Details

Yang, G., Hung, W. N., Song, X., & Guo, W. (2013). A transformation-based approach to implication of GSTE assertion graphs. Journal of Applied Mathematics, 2013.