Don´t cares in logic minimization of extended finite state machines

Extended finite state machines (EFSMs) have been proposed to model control oriented systems. A version of this, with the data portion modeled by Presburger arithmetic, has been used in formal verification and test pattern generation. This paper proposes a general logic minimization scheme using don´t care derived from both control and data path. It consists of methods to transfer don´t cares through the data path and to generate logic don´t cares from the data path using quantifier-free Presburger inequalities. Potential applications are discussed and preliminary results validate the scheme on reasonable examples.