Translating LTL specification to MDG-HDL

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.