Translating LTL specification to MDG-HDL

Author

Wang, Fang ; Habibi, Ali ; Tahar, Sofiene

Author_Institution

ECE Dept., Concordia Univ., Montreal, Que., Canada

Volume

2

fYear

2003

fDate

4-7 May 2003

Firstpage

1369

Abstract

MDG-HDL is the hardware description language accepted by the multiway decision graphs (MDGs) package. Linear temporal logic (LTL) is a widely used formal language for specifying design properties. To develop an LTL model checking algorithm on MDGs, we first need to translate the LTL specification into an automaton described in MDG-HDL. In this paper, we present and compare two methods for translating LTL specifications to MDG-HDL using two existing tools Wring and LTL2AUT. Experimental results based on a set of benchmark LTL formulas show that the Wring based approach is better than the LTL2AUT implementation with respect to the size of the generated automata but is worse in terms of CPU time used.

Keywords

formal languages; formal specification; graph theory; hardware description languages; temporal logic; CPU time; HDL; LTL model checking algorithm; Wring; formal language; hardware description language; linear temporal logic specification; multiway decision graphs package; Automata; Boolean functions; Central Processing Unit; Concrete; Data structures; Feedback circuits; Formal languages; Formal verification; Hardware design languages; Logic design;

fLanguage

English

Publisher

ieee

Conference_Titel

Electrical and Computer Engineering, 2003. IEEE CCECE 2003. Canadian Conference on

ISSN

0840-7789

Print_ISBN

0-7803-7781-8

Type

conf

DOI

10.1109/CCECE.2003.1226154

Filename

1226154