A Transformation-Based Approach to Implication of GSTE Assertion Graphs
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 alternat...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2013-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2013/709071 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850171897319260160 |
|---|---|
| author | Guowu Yang William N. N. Hung Xiaoyu Song Wensheng Guo |
| author_facet | Guowu Yang William N. N. Hung Xiaoyu Song Wensheng Guo |
| author_sort | Guowu Yang |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-a90a69f7eecb4ebf8a0ed84a71926483 |
| institution | OA Journals |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2013-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-a90a69f7eecb4ebf8a0ed84a719264832025-08-20T02:20:12ZengWileyJournal of Applied Mathematics1110-757X1687-00422013-01-01201310.1155/2013/709071709071A Transformation-Based Approach to Implication of GSTE Assertion GraphsGuowu Yang0William N. N. Hung1Xiaoyu Song2Wensheng Guo3School of Computer Science and Engineering, University of Electronic Science and Technology Chengdu, Sichuan 610054, ChinaSynopsys Inc., Mountain View, CA 94043, USADepartment of ECE, Portland State University, Portland, Oregon, USASchool of Computer Science and Engineering, University of Electronic Science and Technology Chengdu, Sichuan 610054, ChinaGeneralized 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.http://dx.doi.org/10.1155/2013/709071 |
| spellingShingle | Guowu Yang William N. N. Hung Xiaoyu Song Wensheng Guo A Transformation-Based Approach to Implication of GSTE Assertion Graphs Journal of Applied Mathematics |
| title | A Transformation-Based Approach to Implication of GSTE Assertion Graphs |
| title_full | A Transformation-Based Approach to Implication of GSTE Assertion Graphs |
| title_fullStr | A Transformation-Based Approach to Implication of GSTE Assertion Graphs |
| title_full_unstemmed | A Transformation-Based Approach to Implication of GSTE Assertion Graphs |
| title_short | A Transformation-Based Approach to Implication of GSTE Assertion Graphs |
| title_sort | transformation based approach to implication of gste assertion graphs |
| url | http://dx.doi.org/10.1155/2013/709071 |
| work_keys_str_mv | AT guowuyang atransformationbasedapproachtoimplicationofgsteassertiongraphs AT williamnnhung atransformationbasedapproachtoimplicationofgsteassertiongraphs AT xiaoyusong atransformationbasedapproachtoimplicationofgsteassertiongraphs AT wenshengguo atransformationbasedapproachtoimplicationofgsteassertiongraphs AT guowuyang transformationbasedapproachtoimplicationofgsteassertiongraphs AT williamnnhung transformationbasedapproachtoimplicationofgsteassertiongraphs AT xiaoyusong transformationbasedapproachtoimplicationofgsteassertiongraphs AT wenshengguo transformationbasedapproachtoimplicationofgsteassertiongraphs |