Computing the observable equivalence relation of a finite state machine

We present a fast method for computing the observable equivalence relation of a finite Mealy machine, which is required for many simplification techniques. Experimentations made for a large class of circuits show a significant gain in time (by a factor ranging from 1.5 to 12) and memory (by a factor ranging from 1.5 to 3). We use the binary decision diagrams to represent and to manipulate the machine, and the symbolic traversal of the machine for performing the computation. Commonly presented algorithms using this technique are based upon the computation of the inverse image of a set of equivalent states pairs by a Boolean function vector, which is a very expensive operation in time and memory. Our new method drastically minimizes the cost of the inverse image computation for computing these pairs. It consists in rewriting successively the machine for the k-equivalence relations.