Symbolic two-level minimization

In this paper, we present a symbolic minimization procedure to obtain optimal two-level implementations of finite-state machines. Encoding based on symbolic minimization consists of optimizing the symbolic representation, and then transforming the optimized symbolic description into a compatible two-valued representation by satisfying encoding constraints (bitwise logic relations) imposed on the binary codes that replace the symbols. Our symbolic minimization procedure captures the sharing of product terms due to ORing effects in the output part of a two-level implementation of the symbolic cover. Face, dominance, and disjunctive constraints are generated. Product terms are accepted in a symbolic minimized cover only when they induce compatible encoding constraints. At the end, a set of codes that satisfy all constraints is computed. The quality of this synthesis procedure is shown by the fact that the cardinality of the cover obtained by symbolic minimization and of the cover obtained by replacing the codes in the initial cover and then minimizing it with ESPRESSO are very close. Experiments show that in some cases, our procedure improves on the best results of state-of-art tools